[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Early verification and validation of mission critical systems

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

Complex software and systems are pervasive in today’s world. In a growing number of fields they come to play a critical role. In order to provide a high assurance level, verification and validation (V&V) should be considered early in the development process. This paper shows how this can be achieved based on a goal-oriented requirements engineering framework which combines complementary semi-formal and formal notations. This allows the analyst to formalize only when and where needed and also preserves optimal communication with stakeholders and developers.

For the industrial application of the methodology, a supporting toolbox was developed. It consist of a number of tightly integrated tools for performing V&V tasks at requirements level. This is achieved through the use of (1) a roundtrip mapping between the requirements language and the specific formal languages used in the underlying formal tools (such as SAT or constraint solvers) and (2) graphical views using domain-based representations. This paper will focus on two major and representative tools: the Refinement Checker (about verification) and the Animator (about validation).

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
£29.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 includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV version 2: An opensource tool for symbolic model checking. In: International Conference on Computer-Aided Verification (CAV, LNCS 2404), Denmark

  2. Dardenne A, van Lamsweerde A, Fickas S (1993) Goal-directed requirements acquisition. Sci Comput Programm 20(1–2):3–50

    Article  MATH  Google Scholar 

  3. Darimont R, van Lamsweerde A (1996) Formal refinement patterns for goal-driven requirements elaboration. FSE-4—4th ACM Symposium on the Foundations of Software Engineering, San Francisco

  4. Easterbrook S, Lutz RR, Covington R, Kelly J, Ampo Y, Hamilton D (1998) Experiences using lightweight formal methods for requirements modeling. Softw Eng 24(1):4–14

    Article  Google Scholar 

  5. The Standish Group (1995) http://www.standishgroup.com/chaos

  6. European Software Institute (1996) European user survey analysis, report usv_eyr 2.1 espiti project

  7. Jackson D (2000) Automating first-order relational logic, ACM SIGSOFT. In: Proceedings of the Conference Foundations of Software Engineering

  8. Koymans R (1992) Specifying message passing and time-critical systems with temporal logic, lncs 651, Springer-Verlag

  9. Letier E, van Lamsweerde A (2001) Agent-based tactics for goal-oriented requirements elaboration

  10. Letier E, van Lamsweerde A (2002) Deriving operational software specifications from system goals. In: FSE'10: 10th ACM S1GSOFT Symposium on the Foundations of Software Engineering, Charleston

  11. Leveson NG (1995) Safeware, system safety and computers, Addison-Wesley

  12. Lutz RR (1993) Analyzing software requirements errors in safety-critical, embedded systems. IEEE International Symposium on Requirements Engineering. IEEE Computer Society Press, San Diego, CA, pp 126–133

    Google Scholar 

  13. Magee J, Pryce N, Giannakopoulou D, Kramer J (2000) Graphical animation of behavior models. Int Conf Softw Eng pp. 499–508

  14. Manna Z, Pnueli A (1992) The reactive behavior of reactive and concurrent system, Springer-Verlag

  15. McLean J, Heitmeyer C (1995) High assurance computer systems: A research agenda. America in the Age of Information, National Science and Technology Council Committee on Information and Communications Forum, Bethesda

  16. Muller T (2000) Promoting constraints to first-class status. First International Conference on Computational Logic (CL, LNAI 1861), London UK

  17. Ponsard C, Balych N, Massonet P, van Lamsweerde A, Vanderdonckt J (2005) Goal-oriented design of domain control panels. In: 12th International Workshop on Design, Specification and Verification of Interactive Systems, Newcastle, UK

  18. Rushby J (2000) Disappearing formal methods. High-assurance systems engineering symposium. Association for Computing Machinery, Albuquerque, NM, pp 95–96

  19. The Objectiver Tool, http://wwww.objectiver.com

  20. Tran Van H, van Lamsweerde A, Massonet P, Ponsard C (2004) Goal-oriented requirements animation. In: 12th IEEE International Requirements Engineering Conference, Kyoto, Japan

  21. van Lamsweerde A (2001) Goal-oriented requirements engineering: A guided tour

  22. van Lamsweerde A, Darimont R, Letier E (1998) Managing conflicts in goal-driven requirements engineering. IEEE Transactions on Software Engineering, Special Issue on Managing Inconsistency in Software Development

  23. van Lamsweerde A, Letier E (2000) Handling obstacles in goal-oriented requirements engineering. IEEE Trans Softw Eng, Special Issue on Except Handl 26(10)

  24. van Lamsweerde A, Letier E (2003) From object orientation to goal orientation: A paradigm shift for requirements engineering. Radical Innovations of Software & System Engineering, Montery'02 Workshop, Venice, Italy, LNCS

  25. van Lamsweerde A (2000) Requirements engineering in the year 00: a research perspective. In: International Conference on Software Engineering, pp 5–19

Download references

Author information

Authors and Affiliations

  1. CETIC Research Center, Brussels, Belgium

    C. Ponsard, P. Massonet & J. F. Molderez

  2. Centre de Recherche Public Henri Tudor, Kirchberg, Luxembourg

    A. Rifaut

  3. UCL, Brussels, Belgium

    A. van Lamsweerde & H. Tran Van

Authors
  1. C. Ponsard
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. P. Massonet
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. J. F. Molderez
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. A. Rifaut
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. A. van Lamsweerde
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. H. Tran Van
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to C. Ponsard.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Ponsard, C., Massonet, P., Molderez, J.F. et al. Early verification and validation of mission critical systems. Form Method Syst Des 30, 233–247 (2007). https://doi.org/10.1007/s10703-006-0028-8

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-006-0028-8

Keywords

Search

Navigation