DocumentCode :
596161
Title :
Efficient Modelling of Embedded Software Systems and their Formal Verification
Author :
Estivill-Castro, Vladimir ; Hexel, Rene ; Rosenblueth, D.A.
Author_Institution :
Sch. of ICT, Griffith Univ., Nathan, NSW, Australia
Volume :
1
fYear :
2012
fDate :
4-7 Dec. 2012
Firstpage :
428
Lastpage :
433
Abstract :
We propose vectors of finite-state machines whose transitions are labeled by formulas of a common-sense logic as the modeling tool for embedded systems software. We have previously shown that this methodology is very efficient in producing succinct and clear models (e.g., in contrast to plain finite-state machines, Petri nets, or Behavior Trees). We show that we can capture requirements precisely and that we can simulate and validate the models. We can, therefore, directly apply Model-Driven Engineering and deploy the models into software for diverse platforms with full tractability of requirements. Moreover, the sequential semantics of our vector of finite-state machines enables model-checking, formally establishing the correctness of the model. Finally, our approach facilitates systematic Failure Modes and Effects Analysis (FMEA) for diverse target platforms. We demonstrate the effectiveness of our methodology with several examples widely discussed in the software engineering literature and compare this with other approaches, showing that we can prove more properties, and that some claims about verification in such approaches have been exaggerated or are incomplete.
Keywords :
embedded systems; finite state machines; formal specification; formal verification; FMEA; Petri nets; behavior tree; common-sense logic; embedded software system; failure mode and effect analysis; finite state machines; formal verification; model checking; model correctness; model-driven engineering; requirement tractability; software engineering; Atmospheric modeling; Computational modeling; Presses; Pumps; Semantics; Software; Unified modeling language; Software testing; formal methods in software engineering; model-driven engineering; software requirements engineering; verification and validation;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Software Engineering Conference (APSEC), 2012 19th Asia-Pacific
Conference_Location :
Hong Kong
ISSN :
1530-1362
Print_ISBN :
978-1-4673-4930-7
Type :
conf
DOI :
10.1109/APSEC.2012.21
Filename :
6462690
Link To Document :
بازگشت