Skip to main content
Springer Nature Link
Log in

Formal methods integration in software engineering

  • Original Paper
  • Published:
Innovations in Systems and Software Engineering Aims and scope Submit manuscript

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

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

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

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

  3. Perseil I (2009) The C-Method, a software engineering method for avionic real-time systems. PhD thesis, Telecom ParisTech

  4. Jacobson I, Booch G, Rumbaugh JE (1999) Excerpt from “The Unified Software Development Process”: the unified process. IEEE Softw 16(3): 82–90

    Article  Google Scholar 

  5. Filliâtre J-C, Marché C (2007) The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. In: CAV, pp 173–177

  6. Lamport L (2002) Specifying systems: the TLA+ language and tools for hardware and software engineers. Addison-Wesley, USA

    Google Scholar 

  7. Lamport L (2006) The +CAL Algorithm Language. In: +CAL

  8. Object Management Group (2007) Unified modeling language: superstructure. OMG, 2nd edn. available at http://www.omg.org/docs/formal/07-11-02.pdf

  9. OMG (2006) Meta object facility (MOF) core specification, 2nd edn. http://www.omg.org/spec/MOF/2.0/PDF/

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

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

    Google Scholar 

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

    Google Scholar 

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

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

  15. Perseil I, Pautet L (2008) Foundations of a new software engineering method for real-time systems. Innov Syst Softw Eng 4(3): 195–202

    Article  Google Scholar 

  16. SAE AS-2C (2004) SAE architecture analysis and design language (AADL). SAE International, sAE AS5506

  17. SAE AS-2C architecture Description Language Subcommittee (2008) Architecture analysis and design language (AADL) v2-Draft v1.6, SAE AS5506. SAE Aerospace

Download references

Author information

Authors and Affiliations

  1. Telecom ParisTech, 46 rue Barrault, 75013, Paris, France

    Isabelle Perseil & Laurent Pautet

Authors
  1. Isabelle Perseil
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Laurent Pautet
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Isabelle Perseil.

Rights and permissions

Reprints 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

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11334-009-0115-2

Keywords

Search

Navigation