Formal methods integration in software engineering
Tóm tắt
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).
Tài liệu tham khảo
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