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:
Informing Assurance Case Review Through a Formal Interpretation of GSN Core Logic Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

Safety and Security Assessment of Behavioral Properties Using Alloy

verfasst von : Julien Brunel, David Chemouil

Erschienen in: Computer Safety, Reliability, and Security

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

In this paper, we propose a formal approach to supporting safety and security engineering, in the spirit of Model-Based Safety Assessment, using the Alloy language. We first implement a system modeling framework, called Coy, allowing to model system architectures and their behavior with respect to component failures. Then we illustrate the use of Coy by defining a fire detection system example and analyzing some safety and security requirements. An interesting aspect of this approach lies in the “declarative” style provided by Alloy, which allows the lean specification of both the model and its properties.

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 A Combined Safety-Hazards and Security-Threat Analysis Method for Automotive Systems
Nächstes Kapitel Combining MILS with Contract-Based Design for Safety and Security Requirements
Literatur
1.
Arnold, A., Point, G., Griffault, A., Rauzy, A.: The altarica formalism for describing concurrent systems. Fundam. Informaticae 40(2,3), 109–124 (1999)MathSciNetMATH
2.
Bieber, P., Brunel, J.: From safety models to security models: preliminary lessons learnt. In: Bondavalli, A., Ceccarelli, A., Ortmeier, F. (eds.) SAFECOMP 2014. LNCS, vol. 8696, pp. 269–281. Springer, Heidelberg (2014)
3.
Bozzano, M., Villafiorita, A., Aakerlund, O., Bieber, P., Bougnol, C., Böde, E., Bretschneider, M., Cavallo, A., Castel, C., Cifaldi, M., Cimatti, A., Griffault, A., Kehren, C., Lawrence, B., Luedtke, A., Metge, S., Papadopoulos, C., Passarello, R., Peikenkamp, T., Persson, P., Seguin, C., Trotta, L., Valacca, L., Zacco, G.: Esacs: an integrated methodology for design and safety analysis of complex systems. In: Proceedings of ESREL 2003. Balkema publisher (2003)
4.
Brunel, J., Chemouil, D., Mélédo, N., Ibanez, V.: Formal modelling and safety analysis of an avionic functional architecture with alloy. In: Embedded Real Time Software and Systems (ERTSS 2014), Toulouse, France (2014)
5.
Brunel, J., Chemouil, D., Rioux, L., Bakkali, M., Vallée, F.: A viewpoint-based approach for formal safety and security assessment of system architectures. In: 11th Workshop on Model-Driven Engineering, Verification, and Validation (MoDeVVa 2014) hosted by MODELS 2014, vol. 1235 of CEUR-WS, pp. 39–48 (2014)
6.
Brunel, J., Rioux, L., Paul, S., Faucogney, A., Vallée, F.: Formal safety and security assessment of an avionic architecture with alloy. In: Proceedings Third International Workshop on Engineering Safety and Security Systems (ESSS 2014), vol. 150 of Electronic Proceedings in Theoretical Computer Science (EPTCS), pp. 8–19 (2014)
7.
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NUSMV: a new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999) CrossRef
8.
Holzmann, G.J.: The model checker spin. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)CrossRef
9.
Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge (2006)
10.
Lin, A., Bond, M., Clulow, J.: Modeling partial attacks with Alloy. In: Christianson, B., Crispo, B., Malcolm, J.A., Roe, M. (eds.) Security Protocols 2007. LNCS, vol. 5964, pp. 20–33. Springer, Heidelberg (2010) CrossRef
11.
Reynolds, M.C.: Lightweight modeling of java virtual machine security constraints. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 146–159. Springer, Heidelberg (2010) CrossRef
12.
Toahchoodee, M., Ray, I.: Using alloy to analyse a spatio-temporal access control model supporting delegation. Inf. Secur. IET 3(3), 75–113 (2009)CrossRef
Metadaten
Titel
Safety and Security Assessment of Behavioral Properties Using Alloy
verfasst von
Julien Brunel
David Chemouil
Copyright-Jahr
2015
Buch
Computer Safety, Reliability, and Security

Print ISBN: 978-3-319-24248-4

Electronic ISBN: 978-3-319-24249-1

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-24249-1_22