MOdel-based DEsign & Verification for Safety-Critical Embedded Systems

Overview of 54 Selected Research Works

Research work

Year

Publisher

Type

Objective

Validation Method

Ni et al [1]

2015

IEEE

Journal

Formal Verification

Case study of Communication System

Berrani et al [2]

2013

IEEE

Conference

Dynamic Verification

Case study of Traffic lights

Amir et al [3]

2015

IEEE

Conference

Dynamic Verification

Case study of Traffic lights

Andrade et al. [4]

2009

IEEE

Conference

Formal Verification

Case study of pulse-oximeter

Quadri et al. [5]

2012

.

IEEE

Conference

Both (Formal & Dynamic) verification

Case study of Car collision avoidance system

Moreira et al. [6]

2010

IEEE

Conference

Dynamic verification

Case study of Valve component system

Vidal et al. [7]

2009

IEEE

Conference

Dynamic verification

Case study of Viterbi decoder

Linehan and Clarke[8]

2011

Elsevier

Journal

Dynamic Verification

Case study of automotive semiconductor industry

Iqbal et al. [9]

2013

.

Springer

Journal

Dynamic verification

Case study of automated bottle recycling system

Samir et al. [10]

2014

Elsevier

Journal

Static verification

Case study of Real time streaming protocol

Ling et al. [11]

2013

IEEE

Conference

Static Verification

Scenarios

Andre et al [12]

2010

IEEE

Conference

Dynamic Verification

Case study of AMBA AHB-to-ABP bridge

Daniel et al. [13]

2011

ACM

Conference

Static Verification

Case study of Elevator system

Ning et al. [14]

2012

Springer

Conference

Formal Verification

Case study of asynchronous RTS model

Luciano et al [15]

2013

Springer

Journal

Both (Formal & Dynamic) verification

Multiple Case studies

Xiaopu et al [16]

2012

ACM

Conference

Formal Verification

Case study of Telephone system

Erwan et al. [17]

2012

ACM

Conference

Formal Verification

Case study of Railway system

Ouchani et al. [18]

2013

IEEE

Conference

Formal Verification

Case study of audio player system

Louati et al [19]

2015

Springer

Conference

Formal Verification

Scenarios

Kanso and Taha [20]

2014

Elsevier

Journal

Dynamic Verification

Case study of smart card product security

Bill et al [21]

2014

Springer

Conference

Formal Verification

Case study of dining philosophers example

Yu et al [22]

2011

IEEE

Conference

Formal Verification

Scenarios

Boutekkouk et al [23]

2009

IEEE

Conference

Formal Verification

Scenarios

Goknil et al [24]

2013

IEEE

Conference

Dynamic Verification

Case study of Brake By Wire

Peters et al [25]

2014

IEEE

Conference

Dynamic Verification

Communication satellite

Bernardi et al [26]

2013

Elsevier

Journal

Static verification

Railway systems case studies

Mueller et al [27]

2010

Springer

Conference

Dynamic verification

Case study of Adaptive

Cruise Controller

Yang et al [28]

2012

Springer

Journal

Static Verification

Case study of vehicular ad hoc networks

Thapa et al [29]

2010

IEEE

Conference

Dynamic Verification

Case study if Positive train control system

Ricardo et al [30]

2014

IEEE

Conference

Formal Verification

Case study of Fire Prevention System

Ebeid et al [31]

2012

IEEE

Conference

Dynamic verification

Case study of Wireless sensor node

Siveroni et al [32]

2008

IEEE

Conference

Static Verification

Scenario

Banerjee et al [33]

2012

ACM

Conference

Dynamic Verification

Case study of Local Interconnect Network protocol

Koycheva et al [34]

2010

IEEE

Conference

Dynamic Verification

Case study of NXT robot

Drusinsky et al [35]

2008

IEEE

Conference

Dynamic Verification

Scenarios

DRIVER et al [36]

2010

ACM

Journal

Dynamic Verification

Case study of Pacemaker

Tien et al [37]

2013

ACM

Conference

Dynamic Verification

Case study of Car Race System

GAMATIÉ et al [38]

2011

ACM

Journal

Both (Formal & Dynamic) Verification

Case study of Multimedia application

GUILLET et al [39]

2014

ACM

Journal

Formal Verification

Case study of Image processing application

Baresi et al [40]

2012

ACM

Conference

Formal Verification

Case study of car collision avoidance system

Rahman et al [41]

2012

IEEE

Conference

Dynamic Verification

Case study if mobile robot system

Jagadish Suryadevara [42]

2013

IEEE

Conference

Formal Verification

Case study of Anti-lock Braking System (ABS)

Guglielmo et al. [43]

2012

Elsevier

Journal

Dynamic verification

(Experiments on different DUTs e.g. Atm and filter)

Kaeem et al [44]

2012

IEEE

Conference

Formal verification

Case study of football player robot application

Hammad et al [45]

2013

ACM

Conference

Dynamic Verification

Case study of motorized traffic density

Lichen Zhang [46]

2014

IEEE

Conference

Dynamic Verification

Case study of Vehicular Ad-hoc NETwork

Ali et al [47]

2015

IEEE

Conference

Static Verification

Case study of liquid fertilizer mixing plant

Sakairi et al. [48]

2012

IEEE

Conference

Dynamic Verification

Case study of Dual Clutch Transmission

Lecomate et al. [49]

2010

Elsevier

Journal

Dynamic verification

Case study of wireless communication demonstrator

Goknil et al [50]

2013

Springer

Conference

Both

(Formal & Dynamic) Verification

Case study of Brake-By-Wire application.

Qureshi et al [51]

2012

Springer

Conference

Formal Verification

Case study of brake-by-wire

system

Julio et al [52]

2011

Springer

Conference

Dynamic Verification

Case study of Teleoperated_Robot

Ammar et al [53]

2016

IEEE

Conference

Dynamic Verification

Case study of H.263 encoding application

Posse et al [54]

2016

Springer

Journal

Formal Verification

Scenarios




References

[1] Siru Ni, Yi Zhuang, Zining Cao, and Xiangying Kong: Modeling Dependability Features for Real-Time Embedded Systems, IEEE Transactions On Dependable And Secure Computing 2015, Volume 12, Issue 2, Pages 190 – 203.

[2] Samir Berrani, Ahmed Hammad, Hassan Mountassir: Mapping SysML to Modelica to Validate Wireless Sensor Networks Non-Functional Requirements, 11th International Symposium on Programming and Systems (ISPS) 2013, Pages 177-186. DOI: 10.1109/ISPS.2013.6581484

[3] Aamir M. Khan, Frédéric Mallet, Muhammad Rashid: Modeling SystemVerilog Assertions using SysML and CCSL, ESLsyn Conference June 10-11 2015, co-located with DAC, USA.

[4] Ermeson Andrade, Paulo Maciel, Gustavo Callou and Bruno Nogueira: A Methodology for Mapping SysML Activity Diagram to Time Petri Net for Requirement Validation of Embedded Real-Time Systems with Energy Constraints, Third International Conference on Digital Society ICDS 2009, Pages 266-271, DOI: 10.1109/ICDS.2009.19

[5] Imran R. Quadri, Etienne Brosse, Ian Gray, Nicholas Matragkas, Leandro Soares Indrusiak, Matteo Rossi, Alessandra Bagnato and Andrey Sadovykh: MADES FP7 EU Project: Effective High Level SysML/MARTE Methodology for Real-Time and Embedded Avionics Systems, 7th International Workshop Reconfigurable Communication-centric Systems-on-Chip (ReCoSoC) 2012, Pages 1-8, DOI: 10.1109/ReCoSoC.2012.6322882

[6] Tomas G. Moreira, Marco A. Wehrmeister, Carlos E. Pereira, Jean-Francois Petin and Eric Levrat: Automatic Code Generation for Embedded Systems: From UML Specifications to VHDL Code, IEEE 8th International Conference on Industrial Informatics (INDIN) 2010, Pages 1085-1090, DOI: 10.1109/INDIN.2010.5549590

[7] Jorgiano Vidal, Florent de Lamotte, Guy Gogniat, Philippe Soulard and Jean-Philippe Diguet: A co-design approach for embedded system modeling and code generation with UML and MARTE, Conference and Exhibition Design Automation and Test in Europe (DATE) 2009, Pages 226-231, DOI: 10.1109/DATE.2009.5090662

[8] Eamonn Linehan and Siobhan Clarke: An aspect-oriented, model-driven approach to functional hardware verification, Journal of Systems Architecture, Elsevier 2012, Volume 58, Issue 5, Pages 195-208, DOI: 10.1016/j.sysarc.2011.02.001

[9] Muhammad Zohaib Iqbal, Andrea Arcuri and Lionel Briand: Environment modeling and simulation for automated testing of soft real-time embedded software, Software and System Modeling, SPRINGER 2013, DOI: 10.1007/s10270-013-0328-6

[10] Samir Ouchani, Otmane Ait Mohamed and Mourad Debbabi: A formal verification framework for SysML activity diagrams, Experts Systems with Applications 2014, Pages 2713-2728.

[11] Ling Yin, Jing Liu, Zuohua Ding ; Mallet, F., de Simone, R.: Schedulability Analysis with CCSL Specifications, 20th Asia-Pacific Software Engineering Conference (APSEC) 2013, Pages 414-421 DOI: 10.1109/APSEC.2013.62

[12] Charles Andre, Frederic Mallet and Julien DeAntoni: VHDL Observers for Clock Constraint Checking, International Symposium on Industrial Embedded Systems (SIES) 2010, Pages 98-107 DOI: 10.1109/SIES.2010.5551372

[13] Daniel Knorreck and Ludovic Apvrille: TEPE: A SysML Language for Time-Constrained Property Modeling and Formal Verification, ACM SIGSOFT Software Engineering Notes 2011, Volume 36, Issue 1, Pages 1-8 DOI: 10.1145/1921532.1921556

[14] Ning Ge, Marc Pantel and Xavier Cregut: Formal Specification and Verification of Task Time Constraints for Real-Time Systems, LNCS SPRINGER 2012, Volume 7610, Pages 143-157 DOI: 10.1007/978-3-642-34032-1_16

[15] Luciano Baresi, Gundula Blohm, Dimitrios S. Kolovos, Nicholas Matragkas, Alfredo Motta, Richard F. Paige, Alek Radjenovic and Matteo Rossi: Formal verification and validation of embedded systems: the UML-based MADES approach, Software and Systems Modeling SPRINGER 2013, DOI: 10.1007/s10270-013-0330-z

[16] Xiaopu Huang, Qingqing Sun, Jiangwei Li, Minxue Pan and Tian Zhang: An MDE-Based Approach to the Verification of SysML State Machine Diagram, Proceedings of the Fourth Asia-Pacific Symposium on Internetware Software, Article 9, ACM 2012, DOI: 10.1145/2430475.2430484

[17] Erwan Bousse, David Mentre, Benoit Combemale, Benoit Baudry and Takaya Katsuragi: Aligning SysML with the B Method to Provide V&V for Systems Engineering, Proceedings of the Workshop on Model-Driven Engineering, Verification and Validation, ACM 2012, Pages 11-16, DOI: 10.1145/2427376.2427379

[18] Samir Ouchani, Otmane Ait Mohamed and Mourad Debbabi: A Formal Verification Framework for BlueSpec System Verilog, Forum on Specification and Design Languages (FDL) 2013, Pages 1-7.

[19] Aymen Louati, Kamel Barkaoui and Chadlia Jerad: Properties Verification of Real-Time Systems Using UML/MARTE/OCL-RT, Formalisms for Reuse and Systems Integration Advances in Intelligent Systems and Computing, Volume 346, 2015, pp 133-147 DOI: 10.1007/978-3-319-16577-6_6

[20] Bilal Kanso and Safouan Taha: Specification of temporal properties with OCL, Science of Computer programming 2014, Volume 96, Part 4, Pages 527-551 DOI: 10.1016/j.scico.2014.02.029

[21] Robert Bill, Sebastian Gabmeyer, Petra Kaufmann and Martina Seid: Model Checking of CTL-Extended OCL Specifications: Software Language Engineering Lecture Notes in Computer Science 2014, Volume 8706, Pages 221-240 DOI: 10.1007/978-3-319-11245-9_13

[22] Huafeng Yu, Talpin, J. ; Besnard, L. ; Gautier, T. ; Marchand, H. ; Le Guernic, P: Polychronous controller synthesis from MARTE CCSL timing specifications, 9th IEEE/ACM International Conference on Formal Methods and Models for Co-design (MEMOCODE) 2011, Pages 21-30 DOI: 10.1109/MEMCOD.2011.5970507

[23] Fateh Boutekkouk and Mohamed Benmohammed: UML Modeling and Formal Verification of control/data driven Embedded Systems, 14th IEEE International Conference on Engineering of Complex Computer Systems 2014, Pages 311-316 DOI: 10.1109/ICECCS.2009.30

[24] Arda Goknil, Julien DeAntoni, Marie-Agnes Peraldi-Frati, Frederic Mallet: Tool Support for the Analysis of TADL2 Timing Constraints using TimeSquare, International Conference on Engineering of Complex Computer Systems 2013, Pages 145-154 DOI: 10.1109/ICECCS.2013.28

[25] Judith Peters, Robert Wille, Rolf Drechsler: Generating SystemC Implementations for Clock Constraints Specified in UML/MARTE CCSL, 19th International Conference on Engineering of Complex Computer Systems 2014, Pages 116-125 DOI: 10.1109/ICECCS.2014.24

[26] S. Bernardi, F. Flammini, S. Marrone , N. Mazzocca, J. Merseguer, R. Nardone and V. Vittorini: Enabling the usage of UML in the verification of railway systems: The DAM-rail approach, Reliability Engineering & System Safety 2013, Volume 120, Pages 112–126 DOI: 10.1016/j.ress.2013.06.032

[27] Wolfgang Mueller, Alexander Bol, Alexander Krupp, and Ola Lundkvist: Generation of Executable Testbenches from Natural Language Requirement Specifications for Embedded Real-Time Systems, Distributed, Parallel and Biologically Inspired Systems (2010), Volume 329, Pages 78-89 DOI: 10.1007/978-3-642-15234-4_9

[28] Nianhua Yang, Huiqun Yu, Hua Sun and Zhilin Qian: Modeling UML Sequence Diagrams Using Extended Petri Nets, Telecommunication Systems 2012, Volume 51, Issue 2, Pages 147-158 DOI: 10.1007/s11235-011-9424-5

[29] Vidhi Thapa, Eunjee Song and Hanil Kim: An Approach to Verifying Security and Timing Properties in UML Models, 15th IEEE International Conference on Engineering of Complex Computer Systems 2015, Pages 193-202 DOI: 10.1109/ICECCS.2010.10

[30] Ricardo J. Rodriguez, Elena Gomez-Martinez: Model-based Safety Assessment using OCL and Petri Nets, 40th Euromicro Conference on Software Engineering and Advanced Applications 2014, Pages 56-59 DOI: 10.1109/SEAA.2014.36

[31] Emad Ebeid, Davide Quaglia and Franco Fummi: Generation of SystemC/TLM code from UML/MARTE sequence diagrams for verification, IEEE 15th International Symposium on Design and Diagnostics of Electronic Circuits & Systems (DDECS) 2012, Pages 187-190 DOI: 10.1109/DDECS.2012.6219051

[32] Igor Siveroni, Andrea Zisman and George Spanoudakis: Property Specification and Static Verification of UML Models, The Third International Conference on Availability, Reliability and Security 2008, Pages 96-103 DOI: 10.1109/ARES.2008.194

[33] A. Banerjeey S. Ray, P. Dasgupta P and P. Chakrabarti: A Dynamic Assertion-based Verification Platform for Validation of UML designs, ACM SIGSOFT Software Engineering Notes 2012, Volume 37 Issue 1,Pages 1-14 DOI: 10.1145/2088883.2088891

[34] Evelina Koycheva, Annerose Braune and Stefan Hennig: Optimization of Production in an autonomous Robot served Manufacturing Facility” 5th IEEE International Conference Intelligent Systems (IS) 2010 , Pages 414-419 DOI: 10.1109/IS.2010.5548382

[35] Doron Drusinsky, James Bret Michael, Thomas W. Otani and Man-Tak Shing: Validating UML Statechart-Based Assertions Libraries for Improved Reliability and Assurance, Second International Conference on Secure System Integration and Reliability Improvement 2008. Pages 47-51 DOI: 10.1109/SSIRI.2008.54

[36] Cormac Driver, Sean Reilly, Eamonn Linehan, Vinny Cahill,And Siobhan Clarke: Managing Embedded Systems Complexity with Aspect-Oriented Model-Driven Engineering, ACM Transactions on Embedded Computing Systems (TECS) 2010, Volume 10 Issue 2, Article No. 21 DOI: 10.1145/1880050.1880057

[37] Thanh Nguyen Tien, Shin Nakajima and Thang Huynh Quyet: Modeling and Debugging Numerical Constraints of Cyber-Physical Systems Design, Proceedings of the Fourth Symposium on Information and Communication Technology 2013, Pages 251-260 DOI: 10.1145/2542050.2542068

[38] Abdoulaye Gamatié, Sébastien Le Beux, Éric Piel, Rabie Ben Atitallah, Anne Etien, Philippe Marquet, and Jean-Luc Dekeyser: A Model-Driven Design Framework for Massively Parallel Embedded Systems, ACM Transactions on Embedded Computing Systems (TECS) 2011, Volume 10 Issue 4, Article No. 39. DOI: 10.1145/2043662.2043663

[39] Sebastien Guillet, Florent De Lamotte, Nicolas Le Griguer, Eric Rutten, Guy Gogniat And Jean-Philippe Diguet: Extending UML/MARTE to Support Discrete Controller Synthesis,Application to Reconfigurable Systems-on-Chip Modeling, ACM Transactions on Reconfigurable Technology and Systems 2014, Volume 7 Issue 3, Article No. 27 DOI: 10.1145/2629628

[40] Luciano Baresi, Angelo Morzenti, Alfredo Motta, Matteo Rossi and Politecnico di Milano: A Logic-based Semantics for the Verification of Multi-diagram UML Models, ACM SIGSOFT Software Engineering Notes 2012, Volume 37 Issue 4, Pages 1-8 DOI: 10.1145/2237796.2237811

[41] Mohd Azizi Abdul Rahman, Nur Safwati Mohd Nor and Makoto Mizukawa: Evaluation for SysML-based Design and Analysis Models Using PCE, IEEE International Conference on Control System, Computing and Engineering (ICCSCE) 2012, Pages 339-344 DOI: 10.1109/ICCSCE.2012.6487167

[42] Jagadish Suryadevara: Validating East-ADL Timing Constraints using UPPAAL, 39th Euromicro Conference Series on Software Engineering and Advanced Applications 2013, Pages 268-275 DOI: 10.1109/SEAA.2013.46

[43] Giuseppe Di Guglielmo, Luigi Di Guglielmo, Andreas Foltinek,, Masahiro Fujita, Franco Fummi, Cristina Marconcini and Graziano Pravadelli: On the integration of model-driven design and dynamic assertion-based verification for embedded software, Journal of Systems and Software, Volume 86, Issue 8, August 2013, Pages 2013–2033. DOI: 10.1016/j.jss.2012.08.061

[44] Yessine Hadj Kacem, Adel Mahfoudhi, Amina Magdich, Chokri Mraidha and Walid Karamti: Using MDE and Priority Time Petri Nets for the schedulability analysis of

Embedded Systems modeled by UML activity diagrams, 19th International Conference and Workshops on Engineering of Computer-Based Systems 2012, Pages 316 – 323 DOI: 10.1109/ecbs.2012.6487436

[45] Ahmed Hammad , Hassan Mountassir and Samir Chouali: An Approach Combining SysML and Modelica for Modelling and Validate Wireless Sensor Networks, Proceedings of the First International Workshop on Software Engineering for Systems-of-Systems 2013, Pages 5-12 DOI: 10.1145/2489850.2489852

[46] Lichen Zhang: Modeling Large Scale Complex Cyber Physical Control Systems Based On System of Systems Engineering Approach, Proceedings of the 20th International Conference on Automation & Computing 2014, Pages 55 – 60 DOI: 10.1109/IConAC.2014.6935460

[47] Sajjad Ali, Muhammad Abdul Basit-Ur-Rahim and Fahim Arif: Formal verification of Time Constrains SysML Internal Block Diagram using PRISM, 15th International Conference on Computational Science and Its Applications 2015, Pages 62-66 DOI: 10.1109/ICCSA.2015.11

[48] Takashi Sakairi, Eldad Palachi, Chaim Cohen, Yoichi Hatsutori, Junya Shimizu, and Hisashi Miyashita: Designing a control system using SysML and Simulink, Proceedings of SICE Annual Conference 2012, Pages 2011-2017

[49] Stéphane Lecomte, Samuel Guillouard, Christophe Moy, Pierre Leray and Philippe Soulard: A co-design methodology based on model driven architecture for real time embedded systems, Mathematical and Computer Modelling 2011, Volume 53, Issues 3–4, Pages 471–484 DOI: 10.1016/j.mcm.2010.03.035

[50] Arda Goknil, Jagadish Suryadevara, Marie-Agnes Peraldi-Frati, Frederic Mallet: Analysis Support for TADL2 Timing Constraints on EAST-ADL Models, Proceedings of the 7th European conference on Software Architecture 2013, Pages 89-105 DOI: 10.1007/978-3-642-39031-9_8

[51] Tahir Naseer Qureshi, De-Jiu Chen, and Martin Törngren: A Timed Automata-Based Method to Analyze EAST-ADL Timing Constraint Specifications, Lecture Notes in Computer Science 2012, Volume 7349, Pages 303-318 DOI: 10.1007/978-3-642-31491-9_23

[52] Julio L. Medina and Alvaro Garcia Cuesta: Model-Based Analysis and Design of Real-Time Distributed Systems with Ada and the UML Profile for MARTE, Lecture Notes in Computer Science 2011, Volume 6652, Pages 89-102 DOI: 10.1007/978-3-642-21338-0_7

[53] Manel Ammar, Mouna Baklouti, Maxime Pelcat, Karol Desnos and Mohamed Abid, On Exploiting Energy-Aware Scheduling Algorithms for MDE-based Design Space Exploration of MP2SoC , 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP), 2016, Pages 643 – 650

[54] Ernesto Posse and Juergen Dingel : An executable formal semantics for UML-RT , Software & Systems Modeling, February 2016, Volume 15, Issue 1, pp 179-217








Back