nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

Evolution of Formal Model-Based Assurance Cases for Autonomous Robots

verfasst von : Mario Gleirscher, Simon Foster, Yakoub Nemouchi

Erschienen in: Software Engineering and Formal Methods

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

An assurance case should carry sufficient evidence for a compelling argument that a system fulfils its guarantees under specific environmental assumptions. Assurance cases are often subject of maintenance, evolution, and reuse. In this paper, we demonstrate how evidence of an assurance case can be formalised, and how an assurance case can be refined using this formalisation to increase argument confidence and to react to changing operational needs. Moreover, we propose two argument patterns for construction and extension and we implement these patterns using the generic proof assistant Isabelle. We illustrate our approach for an autonomous mobile ground robot. Finally, we relate our approach to international standards (e.g. DO-178C, ISO 26262) recommending the delivery and maintenance of assurance cases.

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 Automatic Failure Explanation in CPS Models

Nächstes Kapitel Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management

From the Rodin tool and from LTL and timed CTL checkers.

Usually structured, balanced, and exhibiting many further argumentation qualities.

See https://www.omg.org/spec/SACM/2.0/.

See https://claimsargumentsevidence.org.

The steps 3 and 4 imply that the concrete safety guarantees strengthen the abstract safety guarantees, that is,

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-30446-1_5/478048_1_En_5_IEq159_HTML.gif

In the CPM model, environmental changes are encoded by \(mon := *\), see [13].

CyPhyAssure Project: https://www.cs.york.ac.uk/circus/CyPhyAssure/.

Basir, N.: Safety cases for the formal verification of automatically generated code. Ph.D. thesis, University of Southampton (2010)

Bate, I., Kelly, T.: Architectural considerations in the certification of modular systems. Reliab. Eng. Syst. Saf. 81(3), 303–324 (2003). https://doi.org/10.1016/S0951-8320(03)00094-2CrossRef

Brucker, A.D., Ait-Sadoune, I., Crisafulli, P., Wolff, B.: Using the isabelle ontology framework. In: Rabe, F., Farmer, W.M., Passmore, G.O., Youssef, A. (eds.) CICM 2018. LNCS (LNAI), vol. 11006, pp. 23–38. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96812-4_3CrossRef

Calinescu, R., Weyns, D., Gerasimou, S., Iftikhar, M.U., Habli, I., Kelly, T.: Engineering trustworthy self-adaptive software with dynamic assurance cases. IEEE Trans. Softw. Eng. 44(11), 1039–1069 (2018). https://doi.org/10.1109/tse.2017.2738640CrossRef

Common Criteria Consortium: Common criteria for information technology security evaluation - part 1: Introduction and general model, Technical report, CCMB-2017-04-001 (2017). https://www.commoncriteriaportal.org

Cooper, D., et al.: Tokeneer ID Station: Formal Specification, Technical report, Praxis High Integrity Systems, August 2008. https://www.adacore.com/tokeneer

Denney, E., Pai, G., Habli, I.: Dynamic safety cases for through-life safety assurance. In: 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering. IEEE, May 2015. https://doi.org/10.1109/icse.2015.199

Desai, A., Saha, I., Yang, J., Qadeer, S., Seshia, S.A.: DRONA: a framework for safe distributed mobile robotics. In: Proceedings of the 8th International Conference on Cyber-Physical Systems - ICCPS 2017. ACM Press (2017). https://doi.org/10.1145/3055004.3055022

Edwards, S., Lavagno, L., Lee, E.A., Sangiovanni-Vincentelli, A.: Design of embedded systems: formal models, validation, and synthesis. Proc. IEEE 85(3), 366–90 (1997). https://doi.org/10.1109/5.558710CrossRef

10.

Foster, S., Baxter, J., Cavalcanti, A., Woodcock, J., Zeyda, F.: Unifying semantic foundations for automated verification tools in Isabelle/UTP. Submitted to Science of Computer Programming, March 2019. https://arxiv.org/abs/1905.05500

11.

Foster, S., Zeyda, F., Nemouchi, Y., Ribeiro, P., Wolff, B.: Isabelle/UTP: mechanised theory engineering for unifying theories of programming. Arch. Formal Proofs (2019). https://www.isa-afp.org/entries/UTP.html

12.

Gleirscher, M., Carlan, C.: Arguing from hazard analysis in safety cases: a modular argument pattern. In: 18th International Symposium High Assurance Systems Engineering (HASE), January 2017. https://doi.org/10.1109/hase.2017.15

13.

Gleirscher, M., Foster, S., Nemouchi, Y.: Evolution of formal model based assurance cases for autonomous robots. University of York (2019). Supplemental material. https://doi.org/10.5281/zenodo.3344489

14.

Gleirscher, M., Foster, S., Woodcock, J.: New opportunities for integrated formal methods. ACM Comput. Surv. (2019, inpress). ISSN. 0360-0300. https://arxiv.org/abs/1812.10103

15.

Gleirscher, M., Vogelsang, A., Fuhrmann, S.: A model-based approach to innovation management of automotive control systems. In: 8th International Workshop on Software Product Management (IWSPM). IEEE digital library (2014). https://doi.org/10.1109/IWSPM.2014.6891062

16.

Hawkins, R., Habli, I., Kolovos, D., Paige, R., Kelly, T.: Weaving and assurance case from design: a model-based approach. In: Proceedings of the 16th International Symposium on High Assurance Systems Engineering. IEEE (2015)

17.

Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall, Upper Saddle River (1998)MATH

18.

Jackson, M.A.: Problem Frames: Analysing and Structuring Software Development Problems. Addison-Wesley, Boston (2001)

19.

Kelly, T.: Arguing Safety - A Systematic Approach to Safety Case Management, Ph.D. thesis, University of York (1998)

20.

Kelly, T.P., McDermid, J.A.: Safety case construction and reuse using patterns. In: Daniel, P. (ed.) Safe Comp 97, pp. 55–69. Springer, London (1997). https://doi.org/10.1007/978-1-4471-0997-6_5CrossRef

21.

Lee, E.A., Sirjani, M.: What good are models? In: Bae, K., Ölveczky, P.C. (eds.) FACS 2018. LNCS, vol. 11222, pp. 3–31. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02146-7_1CrossRef

22.

Leveson, N.G.: Engineering a Safer World: Systems Thinking Applied to Safety. MIT Press, Cambridge (2012). https://doi.org/10.7551/mitpress/8179.001.0001. Engineering SystemsCrossRef

23.

Loos, S.M., Platzer, A.: Differential refinement logic. In: Proceeding of the 31st International Symposium on Logic in Computer Science (LICS). ACM, July 2016

24.

Lyons, D.M., Arkin, R.C., Jiang, S., Liu, T.M., Nirmal, P.: Performance verification for behavior-based robot missions. IEEE Trans. Robot. 31(3), 619–636 (2015). https://doi.org/10.1109/tro.2015.2418592CrossRef

25.

Meyer, B.: Applying “design by contract”. IEEE Comput. 25(10), 40–51 (1992)CrossRef

26.

Mitsch, S., Ghorbal, K., Vogelbacher, D., Platzer, A.: Formal verification of obstacle avoidance and navigation of ground robots, CoRR (2016). http://arxiv.org/abs/1605.00604

27.

Nair, S., de la Vara, J.L., Sabetzadeh, M., Falessi, D.: Evidence management for compliance of critical systems with safety standards: a survey on the state of practice. Inf. Softw. Technol. 60, 1–15 (2015). https://doi.org/10.1016/j.infsof.2014.12.002CrossRef

28.

Nemouchi, Y., Foster, S., Gleirscher, M., Kelly, T.: Mechanised assurance cases with integrated formal methods in Isabelle. In: Submitted to iFM 2019 (2019). https://arxiv.org/abs/1905.06192

29.

Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9CrossRefMATH

30.

de Oliveira, A.L., Braga, R.T., Masiero, P.C., Papadopoulos, Y., Habli, I., Kelly, T.: Supporting the automated generation of modular product line safety cases. Adv. Intell. Syst. Comput. 365, 319–330 (2015). https://doi.org/10.1007/978-3-319-19216-1_30CrossRef

31.

Palin, R., Habli, I.: Assurance of automotive safety – a safety case approach. In: Schoitsch, E. (ed.) SAFECOMP 2010. LNCS, vol. 6351, pp. 82–96. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15651-9_7CrossRef

32.

Parnas, D.L., Madley, J.: Function documents for computer systems. Sci. Comput. Program. 25, 41–61 (1995)CrossRef

33.

Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reasoning 41, 143–189 (2008)MathSciNetCrossRef

34.

Prokhorova, Y., Laibinis, L., Troubitsyna, E.: Facilitating construction of safety cases from formal models in event-B. Inf. Softw. Technol. 60, 51–76 (2015). https://doi.org/10.1016/j.infsof.2015.01.001CrossRef

35.

Rahimi, M., Xiadong, X.: A framework for software safety verification of industrial robot operations. Comput. Ind. Eng. 20(2), 279–287 (1991). https://doi.org/10.1016/0360-8352(91)90032-2CrossRef

36.

RTCA: DO-333: Formal Methods Supplement to DO-178C and DO-278A (2012)

37.

Smith, R.S., Doyle, J.C.: Model validation: a connection between robust control and identification. IEEE Trans. Autom. Control 37(7), 942–952 (1992). https://doi.org/10.1109/9.148346MathSciNetCrossRefMATH

38.

Spivey, J.: The Z Notation: A Reference Manual. Prentice Hall, Upper Saddle River (1992)MATH

39.

Wei, R., Kelly, T., Dai, X., Zhao, S., Hawkins, R.: Model based system assurance using the structured assurance case metamodel. J. Softw. Syst. 154, 211–233 (2019)CrossRef

40.

Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice Hall, Upper Saddle River (1996)MATH

Titel: Evolution of Formal Model-Based Assurance Cases for Autonomous Robots
verfasst von: Mario Gleirscher
Simon Foster
Yakoub Nemouchi
Verlag: Springer International Publishing
Buch: Software Engineering and Formal Methods
Print ISBN: 978-3-030-30445-4

Electronic ISBN: 978-3-030-30446-1

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-30446-1_5

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner