UML Modeling and Formal Verification of Control/Data Driven Embedded Systems

Author

Boutekkouk, Fateh ; Benmohammed, Mohamed

Author_Institution

Dept. of Comput. Sci., Univ. of Larbi Ben M´´hedi, Oum El Bouaghi

fYear

2009

fDate

2-4 June 2009

Firstpage

311

Lastpage

316

Abstract

In this paper, we present our approach for UML based modeling of control/data driven embedded systems. In our case application is presented as a network of hierarchic data driven and control driven tasks that communicate via abstract channels. Hardware platform is modeled as UML structure diagram. Mapping of application on hardware platform is modeled through UML constraints. From UML models, a Maude specification is generated. We use this formal specification to formally validate system functionality against some undesirable properties and to estimate system power consumption at a high level of abstraction.

Keywords

Unified Modeling Language; embedded systems; formal specification; program verification; Maude specification; UML modeling; UML structure diagram; abstract channel; control-data driven embedded system; formal specification; formal verification; power consumption estimation; Application software; Computer architecture; Electronic switching systems; Embedded system; Energy consumption; Formal verification; Hardware; Logic; Power system modeling; Unified modeling language; Embedded Systems; Formal Verification; Maude; Power Consumption; Rewriting Logic; UML;

fLanguage

English

Publisher

ieee

Conference_Titel

Engineering of Complex Computer Systems, 2009 14th IEEE International Conference on

Conference_Location

Potsdam

Print_ISBN

978-0-7695-3702-3

Type

conf

DOI

10.1109/ICECCS.2009.30

Filename

5090540