Abstract
This paper presents an extract from our works on a software engineering method for avionic real-time systems [3], the C-Method, which covers the whole software lifecycle thanks to a seamless process, and integrates formal methods in its process. Because distributed, real-time and embedded (DRE) systems have safety critical concerns, they require the use of formal languages (that allow non-ambiguous and rigorous specifications) in order to be able to prove their non-functional properties. Therefore, the “C-Method” relies on the use of formal languages in the earliest steps of the system specification and on the use of semi-formal languages in the analysis, design and programming steps. The fundamental question is how to integrate several languages with different levels of formalization and abstraction. The previous software engineering methods were based on a single language or notation, so they did not address this issue. In order to make the transitions more continuous between semi-formal and formal specifications, we have introduced in the development process what we call “intermediate” languages (+CAL and Why), that are easy to manipulate but directly linked to a formal language (TLA+ for +CAL, Why for PVS).
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Faugere M, Bourbeau T, de Simone R, Gerard S (2007) MARTE: also an UML profile for modeling AADL applications. In: ICECCS ’07: proceedings of the 12th IEEE international conference on engineering complex computer systems (ICECCS 2007). IEEE Computer Society, Washington, pp 359–364. doi:10.1109/ICECCS.2007.29
Gerard S, Feiler P, Rolland J, Filali M, Reiser MO, Delanote D, Berbers Y, Pautet L, Perseil I (2007) UML&AADL ’2007 Grand Challenges. ACM SIGBED Review, A Special Report on UML&AADL Grand Challenges 4(4)
Perseil I (2009) The C-Method, a software engineering method for avionic real-time systems. PhD thesis, Telecom ParisTech
Jacobson I, Booch G, Rumbaugh JE (1999) Excerpt from “The Unified Software Development Process”: the unified process. IEEE Softw 16(3): 82–90
Filliâtre J-C, Marché C (2007) The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. In: CAV, pp 173–177
Lamport L (2002) Specifying systems: the TLA+ language and tools for hardware and software engineers. Addison-Wesley, USA
Lamport L (2006) The +CAL Algorithm Language. In: +CAL
Object Management Group (2007) Unified modeling language: superstructure. OMG, 2nd edn. available at http://www.omg.org/docs/formal/07-11-02.pdf
OMG (2006) Meta object facility (MOF) core specification, 2nd edn. http://www.omg.org/spec/MOF/2.0/PDF/
Owre S, Rushby JM, Shankar N (1992) PVS: a prototype verification system. In: CADE-11: proceedings of the 11th international conference on automated deduction. Springer, London, pp 748–752
Paige RF (1997) A meta-method for formal method integration. In: Fitzgerald JS, Jones CB, Lucas P (eds) FME. Lecture notes in computer science, vol 1313. Springer, Graz, pp 473–494
Paige RF (1997) Case studies in using a meta-method for formal method integration. In: Johnson M (eds) AMAST. Lecture notes in computer science, vol 1349. Springer, Sydney, pp 395–408
Perseil I, Pautet L (2007) A Co-Modeling Methodology Designed for RT Architecture Models Integration. In: Society IC (ed) 12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007), pp 371–376
Perseil I, Pautet L (2008) A concrete syntax for UML 2.1 action semantics using +CAL. In: 13th international conference on engineering of complex computer systems, ICECCS. IEEE Computer Society, Belfast, pp 217–221
Perseil I, Pautet L (2008) Foundations of a new software engineering method for real-time systems. Innov Syst Softw Eng 4(3): 195–202
SAE AS-2C (2004) SAE architecture analysis and design language (AADL). SAE International, sAE AS5506
SAE AS-2C architecture Description Language Subcommittee (2008) Architecture analysis and design language (AADL) v2-Draft v1.6, SAE AS5506. SAE Aerospace
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Perseil, I., Pautet, L. Formal methods integration in software engineering. Innovations Syst Softw Eng 6, 5–11 (2010). https://doi.org/10.1007/s11334-009-0115-2
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11334-009-0115-2