Paper Info
Title
Formal Verification for Embedded Systems Design Based on MDE
Abstract
This work presents a Model Driven Engineering (MDE) approach for the automatic generation of a network of timed automata from the functional specification of an embedded application described using UML class and sequence diagrams. By means of transformations on the UML model of the embedded system, a MOF-based representation for the network of timed automata is automatically obtained, which can be used as input to formal verification tools, as the Uppaal model checker, in order to validate desired functional and temporal properties of the embedded system specification. Since the network of timed automata is automatically generated, the methodology can be very useful for the designer, making easier the debugging and formal validation of the system specification. The paper describes the defined transformations between models, which generate the network of timed automata as well as the textual input to the Uppaal model checker, and illustrates the use of the methodology with a case study to show the effectiveness of the approach.
Year
DOI
Venue
2009
10.1007/978-3-642-04284-3_15
ANALYSIS, ARCHITECTURES AND MODELLING OF EMBEDDED SYSTEMS
Keywords
Field
DocType
model driven engineering,sequence diagram,embedded system,formal verification
Sequence diagram,Model checking,Programming language,Unified Modeling Language,Model-driven architecture,Computer science,System requirements specification,Functional specification,Debugging,Formal verification,Embedded system
Conference
Volume
ISSN
Citations 
310
1868-4238
4
PageRank 
References 
Authors
0.43
11
3
Name
Order
Citations
PageRank
Francisco Assis M. Do Nascimento1373.97
Marcio Ferreira da Silva Oliveira240.43
Flávio Rech Wagner338059.82