Abstract
The paper 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 [1], [2]. 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 user-friendly. Each method is applied on a suitable case study, that we regret some missing features we could found 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 [3] and the temporal logic FNLOG [7]. 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 [7]. The proposed integration approach uses the notations of STATEMATE and FNLOG, defines a various transformations rules of a STATEMATE specification towards FNLOG and extends the axiomatic of the temporal logic FNLOG by new lemmas to deal with duration properties. The paper presents the various steps of our integration approach.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
E.M. Clarke and J.M. Wing, Formal Methods: state of the art and Future Directions, ACMcomputing survey, Vol. 28, N0 4, P 626–643, décembre 1996.
B. Cohen, A brief history of formal methods, FACS Europe, Vol. 1, N0 3, 1994.
D. Harel, Modeling Reactive systems with Statecharts: The statemate approach, McGraw-Hill, USA, 1997.
T.A. Henzinger, Z. Manna and A. Pnueli, Temporal Proof Methodologies for Real-Time Systems, 18 th Ann. Syym on Principales of Programming Languages, P 353–366, ACM Press, 1991.
F. Jahanian and A.K.-L. Mok, Safety analysis of timing properties in Real-time systems, I.E.E.E Trans. On soft. Eng., Vol. 12, N0 9, P 890–904, 1986.
O. Mosbah1i, Une technique de spécification et de validation basée sur la méthode STATEMATE et la logique FNLOG, mémoire de D.E.A en informatique, FST, Tunis, Tunisie, 2002.
A. Sowmya and S. Ramesh, A Semantics-Preserving Transformation of statecharts to FNLOG, Proc.14 th. IFAC Workshop Distributed Computer Control systems, Seoul, Korea, 1977.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mosbahi, O., Jemni, L., Ahmed, S.B., Jaray, J. (2002). A Specification and Validation Technique Based on STATEMATE and FNLOG. In: George, C., Miao, H. (eds) Formal Methods and Software Engineering. ICFEM 2002. Lecture Notes in Computer Science, vol 2495. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36103-0_23
Download citation
DOI: https://doi.org/10.1007/3-540-36103-0_23
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00029-7
Online ISBN: 978-3-540-36103-9
eBook Packages: Springer Book Archive