From graphical design in STATEMATE to formal specification in Event B

Author

Ben Ayed, Leila Jemni ; Ben Younes, Ahlem

Author_Institution

Unite de Recherche en Technol. de I´´Inf. et de la Commun., Ecole Superieure des Sci. et Techniques de Tunis

Volume

2

fYear

0

fDate

0-0 0

Firstpage

2837

Lastpage

2842

Abstract

In this paper, we present a specification technique borrowing features from two classes of specification methods, formal and semi-formal ones. The proposed technique uses STATEMATE as semi formal method and the Event B as formal one. The design is initially expressed graphically with STATEMATE, then translated to Event B and verified using powerful support tools of the B method. This paper presents a scheme for the translation of statecharts and communication between activity-charts to Event B method. We propose a solution to specify time in the event based B method and a derivation of temporal expressions (timeout in statecharts) to Event B. By an example of a real time system, we illustrate our technique

Keywords

formal specification; formal verification; STATEMATE; activity-chart; event B method; formal specification; graphical design; semiformal specification; statechart; temporal expression; Concurrent computing; Control system synthesis; Embedded system; Formal specifications; Libraries; Programming; Real time systems; Software safety; Software standards; Software systems;

fLanguage

English

Publisher

ieee

Conference_Titel

Information and Communication Technologies, 2006. ICTTA '06. 2nd

Conference_Location

Damascus

Print_ISBN

0-7803-9521-2

Type

conf

DOI

10.1109/ICTTA.2006.1684862

Filename

1684862