FORMAL METHOD FOR AUTOMATED TRANSFORMATION OF LOTOS SPECIFICATIONS TO ESTELLE SPECIFICATIONS

2005 ◽  
Vol 15 (05) ◽  
pp. 873-891 ◽  
Author(s):  
HAZEM EL-GENDY ◽  
NABIL EL-KADHI
Keyword(s):  
Real Time ◽  
Formal Method ◽  
Conformance Testing ◽  
Control Flow ◽  
Semantic Model ◽  
Formal Description ◽  
Real Time Systems ◽  
Behavior Tree ◽  
Time Systems ◽  
Formal Description Techniques

ISO and IEC have jointly developed two Formal Description Techniques (FDTs) for specifying distributed real time systems such as computer/telecommunications protocols. These are Lotos and Estelle. In this paper, a formal method for automated transformation of a Lotos specification to an Estelle specification is presented. The method is applicable to various Lotos specification styles and to various communications protocols of ISO OSI layers. Our method has applications in conformance testing of such systems and building common semantic model for the various FDTs. In this paper, we develop an algorithm for constructing a 'Data Oriented'-Restricted Behavior Tree T that represent both the control flow aspects and the data flow aspects of the system. Then, we develop an algorithm for constructing the Estelle specifications from T. A minimization rule is also developed to optimize the size of the Estelle specification by reducing both the number of states and the number of transitions.

Conformance testing for real-time systems

2009 ◽  
Vol 34 (3) ◽  
pp. 238-304 ◽  
Author(s):  
Moez Krichen ◽  
Stavros Tripakis
Keyword(s):  
Real Time ◽  
Conformance Testing ◽  
Real Time Systems ◽  
Time Systems

Sokrates-SA - A formal method for specifying real-time systems

1989 ◽  
Vol 27 (1-5) ◽  
pp. 513-520 ◽  
Author(s):  
Ari Okkonen ◽  
Antti Auer ◽  
Mikko Levanto ◽  
Jyrki Okkonen ◽  
Jarmo Kalaoja
Keyword(s):  
Real Time ◽  
Formal Method ◽  
Real Time Systems ◽  
Time Systems

A Language for Formal Description of Real Time Systems

1983 ◽  
Vol 16 (18) ◽  
pp. 119-126
Author(s):  
F. Boussinot ◽  
R. Martin ◽  
G. Memmi ◽  
G. Ruggiu ◽  
J. Vapné
Keyword(s):  
Real Time ◽  
Formal Description ◽  
Real Time Systems ◽  
Time Systems

A LANGUAGE FOR FORMAL DESCRIPTION OF REAL TIME SYSTEMS

1983 ◽  
pp. 119-126 ◽  
Author(s):  
F. Boussinot ◽  
R. Martin ◽  
G. Memmi ◽  
G. Ruggiu ◽  
J. Vapné
Keyword(s):  
Real Time ◽  
Formal Description ◽  
Real Time Systems ◽  
Time Systems

Specification and Validation of Real Time Systems

2011 ◽  
pp. 444-475
Author(s):  
Olfa Mosbahi
Keyword(s):  
Real Time ◽  
Formal Methods ◽  
Temporal Logic ◽  
Formal Method ◽  
The Other ◽  
Real Time Systems ◽  
Critical Systems ◽  
Temporal Properties ◽  
Integration Approach ◽  
Time Systems

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).

scholarly journals Effortless Fault Localisation: Conformance Testing of Real-Time Systems in Ecdar

2018 ◽  
Vol 277 ◽  
pp. 147-160 ◽  
Author(s):  
Tobias R. Gundersen ◽  
Florian Lorber ◽  
Ulrik Nyman ◽  
Christian Ovesen
Keyword(s):  
Real Time ◽  
Conformance Testing ◽  
Real Time Systems ◽  
Time Systems
Sign in / Sign up

Export Citation Format

Share Document