Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Temporal Logic Framework for Performance Analysis of Architectures of Systems Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

From Design Contracts to Component Requirements Verification

verfasst von : Jing Liu, John D. Backes, Darren Cofer, Andrew Gacek

Erschienen in: NASA Formal Methods

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

During the development and verification of complex airborne systems, a variety of languages and development environments are used for different levels of the system hierarchy. As a result, there may be manual steps to translate requirements between these different environments. This paper presents a tool-supported export technique that translates high-level requirements from the software architecture modeling environment into observers of requirements that can be used for verification in the software component environment. This allows efficient verification that the component designs comply with their high-level requirements. It also provides an automated tool chain supporting formal verification from system requirements down to low-level software requirements that is consistent with certification guidance for avionics systems. The effectiveness of the technique has been evaluated and demonstrated on a medical infusion pump and an aircraft wheel braking system.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Semantics for Locking Specifications
Nächstes Kapitel A Hybrid Architecture for Correct-by-Construction Hybrid Planning and Control
Fußnoten
1
For example, if the term \( pre (x)\) appears multiple times in the AGREE contract, we only create a single persistent variable for this expression.
 
Literatur
1.
Cofer, D., Gacek, A., Miller, S., Whalen, M.W., LaValley, B., Sha, L.: Compositional verification of architectural models. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 126–140. Springer, Heidelberg (2012)CrossRef
2.
Whalen, M.W., Gacek, A., Cofer, D.D., Murugesan, A., Heimdahl, M.P.E., Rayadurgam, S.: Your “what” is my “how”: Iteration and hierarchy in system design. IEEE Softw. 30, 54–60 (2013)CrossRef
3.
Feiler, P.H., Gluch, D.P.: Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis & Design Language, 1st edn. Addison-Wesley Professional, Boston (2012)
4.
5.
RTCA DO-178C: Software Considerations in Airborne Systems and Equipment Certification, Washington, DC (2011)
6.
RTCA DO-333: Formal Methods Supplement to DO-178C and DO-278A, Washington, DC (2011)
7.
RTCA DO-331: Model-Based Development and Verification Supplement to DO-178C and DO-278A, Washington, DC (2011)
8.
Cofer, D., Miller, S.P.: Formal methods case studies for DO-333, NASA contractor report NASA/CR-2014-218244 (2014)
9.
10.
Murugesan, A., Whalen, M.W., Rayadurgam, S., Heimdahl, M.P.: Compositional verification of a medical device system. In: ACM International Conference on High Integrity Language Technology (HILT) 2013. ACM (2013)
11.
Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous dataflow programming language LUSTRE. Proc. IEEE 79, 1305–1320 (1991)CrossRef
12.
Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems, 2nd edn. Cambridge University Press, Cambridge (2004)CrossRefMATH
13.
14.
RTCA DO-330: Software Tool Qualification Considerations, Washington, DC (2011)
15.
Miller, S.P., Bhattacharyya, S., Tinelli, C., Smolka, S., Sticksel, C., Meng, B., Yang, J.: Formal verification of quasi-synchronous systems. Final Technical report delivered Air Force Research Laboratory (2015)
16.
Accident, C.A., Incident Investigation Commission (CIAIAC), S.: Technical report: Accident occurred on 21 May 1998 to Aircraft Airbus A-320-21 Registration G-UKLL At Ibiza Airport, Balearic Islands (1998)
17.
18.
Wang, C., Pastore, F., Goknil, A., Briand, L., Iqbal, Z.: Automatic generation of system test cases from use case specifications. In: Proceedings of the 2015 International Symposium on Software Testing and Analysis, ISSTA 2015, pp. 385–396. ACM, New York (2015)
19.
Ibrahim, R., Saringat, M., Ibrahim, N., Ismail, N.: An automatic tool for generating test cases from the system’s requirements. In: 7th IEEE International Conference on Computer and Information Technology, CIT 2007, pp. 861–866 (2007)
20.
Escalona, M.J., Gutierrez, J.J., Mejías, M., Aragón, G., Ramos, I., Torres, J., Domínguez, F.J.: An overview on test generation from functional requirements. J. Syst. Softw. 84, 1379–1393 (2011)CrossRef
21.
Miller, S.P., Tribble, A.C., Whalen, M.W., Heimdahl, M.P.E.: Proving the shalls: early validation of requirements through formal methods. Int. J. Softw. Tools Technol. Transf. 8, 303–319 (2006)CrossRef
22.
Bozzano, M., Cimatti, A., Katoen, J., Katsaros, P., Mokos, K., Nguyen, V.Y., Noll, T., Postma, B., Roveri, M.: Spacecraft early design validation using formal methods. Reliab. Eng. Syst. Saf. 132, 20–35 (2014)CrossRef
23.
Silva, W., Bezerra, E., Winterholer, M., Lettnin, D.: Automatic property generation for formal verification applied to hdl-based design of an on-board computer for space applications. In: 2013 14th Latin American Test Workshop (LATW), pp. 1–6 (2013)
24.
Soeken, M., Kuhne, U., Freibothe, M., Fe, G., Drechsler, R.: Automatic property generation for the formal verification of bus bridges. In: 2011 IEEE 14th International Symposium on Design and Diagnostics of Electronic Circuits Systems (DDECS), pp. 417–422 (2011)
25.
Cimatti, A., Tonetta, S.: Contracts-refinement proof system for component-based embedded systems. Sci. Comput. Program. Part 3 97, 333–348 (2015)CrossRef
Metadaten
Titel
From Design Contracts to Component Requirements Verification
verfasst von
Jing Liu
John D. Backes
Darren Cofer
Andrew Gacek
Copyright-Jahr
2016
Buch
NASA Formal Methods

Print ISBN: 978-3-319-40647-3

Electronic ISBN: 978-3-319-40648-0

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-40648-0_28