Welcome to the InfoSci Platform
Specification and Validation of Real Time Systems

Specification and Validation of Real Time Systems

Olfa Mosbahi
Copyright: © 2011 |Pages: 32
ISBN13: 9781609600860|ISBN10: 160960086X|EISBN13: 9781609600884
DOI: 10.4018/978-1-60960-086-0.ch017
Cite Chapter Cite Chapter

MLA

Mosbahi, Olfa. "Specification and Validation of Real Time Systems." Reconfigurable Embedded Control Systems: Applications for Flexibility and Agility, edited by Mohamed Khalgui and Hans-Michael Hanisch, IGI Global, 2011, pp. 444-475. https://doi.org/10.4018/978-1-60960-086-0.ch017

APA

Mosbahi, O. (2011). Specification and Validation of Real Time Systems. In M. Khalgui & H. Hanisch (Eds.), Reconfigurable Embedded Control Systems: Applications for Flexibility and Agility (pp. 444-475). IGI Global. https://doi.org/10.4018/978-1-60960-086-0.ch017

Chicago

Mosbahi, Olfa. "Specification and Validation of Real Time Systems." In Reconfigurable Embedded Control Systems: Applications for Flexibility and Agility, edited by Mohamed Khalgui and Hans-Michael Hanisch, 444-475. Hershey, PA: IGI Global, 2011. https://doi.org/10.4018/978-1-60960-086-0.ch017

Export Reference

Mendeley
Favorite

Abstract

The chapter presents a specification technique borrowing features from two classes of specification methods, formal and semi-formal ones. Each of the above methods have been proved to be useful in the development of real-time and critical systems and widely reported in different papers (Bruel, 1996; Clarke & Wing, 1996; Cohen, 1994; Fitzgerald & Larsen, 1994; Ghezzi, Mandrioli & Morzenti, 1990). Formal methods are based on mathematical notations and axiomatic which induce verification and validation. Semi-formal methods are, in the other hand, graphic, structural and uer-friendly. Each method is applied on a suitable case study, that we regret some missing features we could find in the other class. This remark has motivated our work. We are interested in the integration of formal and semi-formal methods in order to lay out a specification approach which combines the advantages of theses two classes of methods. The proposed technique is based on the integration of the semi-formal method STATEMATE (Harel, 1997; Harel, 1987) and the temporal logic FNLOG (Sowmya & Ramesh, 1997). This choice is justified by the fact that FNLOG is formal, deals with quantitative temporal properties and that these two approaches have a compatibility which simplifies their integration (Sowmya & Ramesh, 1997). The proposed integration approach uses the notations of STATEMATE and FNLOG, defines various transformation rules of a STATEMATE specification towards FNLOG and extends the axiomatics of the temporal logic FNLOG by new lemmas to deal with duration properties. The chapter presents the various steps of our integration approach, the proposed extentions and illustrates it over a case of critical real-time systems: the gas burner system (Ravn, Rishel & Hansen, 1993).

Request Access

You do not own this content. Please login to recommend this title to your institution's librarian or purchase it from the IGI Global bookstore.