Abstract
A well known challenge in the formal methods domain is to improve their integration with practical engineering methods. In the context of embedded systems, model checking requires first to model the system to be validated, then to formalize the properties to be satisfied, and finally to describe the behavior of the environment. This last point which we name as the proof context is often neglected. It could, however, be of great importance in order to reduce the complexity of the proof. The question is then how to formalize such a proof context. We experiment a language, named CDL (Context Description Language), for describing a system environment using actors and sequence diagrams, together with the properties to be checked. The properties are specified with textual patterns and attached to specific regions in the context. Our contribution is a report on several industrial embedded system applications.
Empirical results category paper.
This is a preview of subscription content, log in via an institution to check access.
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
Alur, R., Dill, D.: A Theory of Timed Automata. Theoretical computer Science 126(2), 183–235 (2004)
Bozga, M., Graf, S., Mounier, L.: IF2: A validation environment for component-based real-time systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 343. Springer, Heidelberg (2002)
Clarke, T., Evans, A., Sammut, P., Willians, J.: Applied Meamodeling: A foundation for Language Driven Development. Technical report, version 0.1, Xactium (2004)
ITU-T. Recommendations Z-100. Specification and Description Language (SDL) (1994)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proc. of the 21st Int. Conf. on Software Engineering, pp. 411–420. IEEE Computer Society Press, Los Alamitos (1999)
Halbwachs, N., Lagnier, F., Raymond, P.: Synchronous observers and the verification of reactive systems. In: 3rd int. Conf. on Algebraic Methodology and Software Technology, AMAST 1993 (1993)
Haugen, O., Husa, K.E., Runde, R.K., Stolen, K.: Stairs: Towards formal design with sequence diagrams. Journal of Software and System Modeling (2005)
Fernandez, J.-C., et al.: CADP: A Protocol Validation and Verification Toolbox. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102. Springer, Heidelberg (1996)
Janssen, W., Mateescu, R., Mauw, S., Fennema, P., Stappen, P.: Model Checking for Managers. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 92–107. Springer, Heidelberg (1999)
Konrad, S., Cheng, B.: Real-Time Specification Patterns. In: Proc. of the 27th Int. Conf. on Software Engineering (ICSE 2005), St Louis, MO, USA (2005)
Roger, J.C.: Exploitation de contextes et d’observateurs pour la vérification formelle de modèles, Phd report, Univ. of Rennes I (2006)
Smith, R., Avrunin, G.S., Clarke, L., Osterweil, L.: Propel: An Approach Supporting Property Elucidation. In: Proc. of the 24th Int. Conf. on Software Engineering, pp. 11–21. ACM Press, New York (2002)
Whittle J.: Specifying precise use cases with use case charts. In MoDELS 2006, Satellite Events, pp. 290–301 (2005)
Berthomieu, B., Vernadat, F.: Time Petri nets analysis with TINA. In: 3rd Int. Conf. on the Quantitative Evaluation of Systems (QEST 2006), Riverside, USA, pp. 123–124 (2006)
Berthomieu, B., Bodeveix, J., Filali, M., Garavel, H., Lang, F., Peres, F., Saad, R., Stoecker, J., Vernadat, F.: The Syntax and Semantics of FIACRE, Version 1.0 alpha. Technical report projet ANR05RNTL03101 OpenEmbeDD (2007)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 2, 244–263 (1986)
Hassine, J., Rilling, J., Dssouli, R.: Use Case Maps as a property specification language. Software System Model 8, 205–220 (2009)
Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Springer, New York (1992)
Feiler, P., Gluch, D.P., Hudak, J.J.: The Architecture Analysis and Design Language (AADL): An introduction.Technical report, Society of Automotive Engineers, SAE (2006)
Dhaussy, P., Boniol, F.: Mise en œuvre de composants MDA pour la validation formelle de modèles de systèmes d’information embarqués, pp. 133–157. RSTI (2007)
Dhaussy P., Auvray J., De Belloy S., Boniol F., Landel E.: Using context descriptions and property definition patterns for software formal verification, Workshop Modevva 2008 (hosted by ICST 2008), Lillehammer, Norway (2008)
Dhaussy, P., Creff, S., Pillain, P.Y., Leilde, V.: CDL language specification (Context Description Language). Technical report version N° DTN/2009/8, ENSIETA (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dhaussy, P., Pillain, PY., Creff, S., Raji, A., Le Traon, Y., Baudry, B. (2009). Evaluating Context Descriptions and Property Definition Patterns for Software Formal Validation. In: Schürr, A., Selic, B. (eds) Model Driven Engineering Languages and Systems. MODELS 2009. Lecture Notes in Computer Science, vol 5795. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04425-0_34
Download citation
DOI: https://doi.org/10.1007/978-3-642-04425-0_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04424-3
Online ISBN: 978-3-642-04425-0
eBook Packages: Computer ScienceComputer Science (R0)