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
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Innovations in Systems and Software Engineering
Erschienen in: Innovations in Systems and Software Engineering 4/2018

22.12.2018 | Original Paper

Formal verification of SysML diagram using case studies of real-time system

verfasst von: Sajjad Ali

Erschienen in: Innovations in Systems and Software Engineering | Ausgabe 4/2018

Einloggen

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

search-config
loading …

Abstract

System and software engineers use SysML models for the graphical modeling of the embedded systems. The SysML models are inadequate to express the discrete controllers with continuously evolving variables. The real-time constraints such as discrete and continuous dynamics are considered to be an important aspect in embedded systems. The lack of support of real-time aspect in SysML model can lead to inexplicit modeling of the embedded systems. The imprecise modeling could cause catastrophic results when an embedded system gets operational. In this paper, we propose hybrid automata-based semantics that supports the discrete and continuous behavior in upgraded SysML block diagram. The upgraded SysML block diagram is used for the modeling of the embedded system. Furthermore, we use model checker PRISM for the early design verification of upgraded SysML block diagram. Finally, we demonstrate the effectiveness of our proposed approach with the help of two case studies “temperature control system” and “water level control system”.
Nächster Artikel Software architectural patterns in practice: an empirical study

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 "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

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
Literatur
1.
Baier C, Katoen J-P (2008) Principles of model checking, vol 26202649. MIT press, CambridgeMATH
2.
3.
4.
Jarraya Y, Soeanu A, Debbabi M, Hassaine F (2007). Automatic verification and performance analysis of time-constrained sysml activity diagrams. In: 14th annual IEEE international conference and workshops on the engineering of computer-based systems, 2007. ECBS ’07, IEEE pp 515–522
5.
Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge
6.
Raskin JF (2005) An introduction to hybrid automata. In: Johansson K, Törngren M, Nielsen L (eds) Handbook of networked and embedded control systems. Birkhauser, Boston, pp 491–517CrossRef
7.
Ouchani S, Mohamed OA, Debbabi M (2013) A probabilistic verification framework of SysML activity diagrams. In: 2013 IEEE 12th international conference on intelligent software methodologies, tools and techniques (SoMeT). IEEE, pp 165–170
8.
Ouchani S, Mohamed OA, Debbabi M (2014) A formal verification framework for sysml activity diagrams. Expert Syst Appl 41(6):2713–2728CrossRef
9.
Ouchani S, Mohamed OA, Debbabi M (2014) A property-based abstraction framework for sysml activity diagrams. Knowl Based Syst 56:328–343CrossRef
10.
Ouchani S, Mohamed OA, Debbabi M (2012) Efficient probabilistic abstraction for SysML activity diagrams. In: Software engineering and formal methods. Springer, Berlin, pp 263–277
11.
Jarraya Y, Debbabi M, Bentahar J (2009). On the meaning of SysML activity diagrams. In: ECBS 2009, 16th annual IEEE international conference and workshop on the engineering of computer based systems, 2009. IEEE, pp 95–105
12.
Debbabi M, Hassaine F, Jarraya Y, Soeanu A, Alawneh L (2010) Probabilistic model checking of SysML activity diagrams. In: Verification and validation in systems engineering. Springer, Berlin, pp 153–166
13.
Jansen DN, Hermanns H, Katoen JP (2002) A probabilistic extension of UML statecharts. In: Formal techniques in real-time and fault-tolerant systems. Springer, Berlin, pp 355–374
14.
Bianco VD, Lavazza L, Mauri M (December 2002) Model checking UML specifications of real time software. In: Eighth IEEE international conference on engineering of complex computer systems, 2002. Proceedings. IEEE, pp 203–212
15.
Basit-Ur-Rahim MA, Arif F, Ahmad J ( January 2014) Formal verification of sequence diagram using divine. In: 2014 World Congress on computer applications and information systems (WCCAIS). IEEE, pp 1–6
16.
Lima V, Talhi C, Mouheb D, Debbabi M, Wang L, Pourzandi M (2009) Formal verification and validation of UML 2.0 sequence diagrams using source and destination of messages. Electron Notes Theor Comput Sci 254:143–160CrossRef
17.
Mazzini S, Puri S, Mari F, Melatti I, Tronci E (2009) Formal verification at system level, DAta Systems in Aerospace (DASIA), Org. EuroSpace, Canadian Space Agency, CNES, ESA, EUMETSAT, Instanbul, Turkey
18.
Soliman D, Thramboulidis K, Frey G (2012) Function block diagram to uppaal timed automata transformation based on formal models. Inf Control Probl Manuf 14(1):1653–1659
19.
Linhares MV, Oliveira RSD, Farines JM, Vernadat F (September 2007) Introducing the modeling and verification process in SysML. In: Emerging technologies and factory automation. IEEE Conference on ETFA 2007. IEEE, pp 344–351
20.
Ali S, Basit-Ur-Rahim MA, Arif F (June 2015) Formal verification of internal block diagram of SysML for modeling real-time system. In: 16th IEEE/ACIS international conference on software engineering, artificial intelligence, networking and parallel/distributed computing (SNPD 2015). IEEE (in press)
21.
Ali S, Basit-Ur-Rahim MA, Arif F (June 2015) Formal verification of time constrains SysML internal block diagram using prism. In: 15th international conference on computational science and its applications (ICCSA 2015). IEEE (in press)
22.
Hinton A, Kwiatkowska M, Norma G, Parker D (2006) Prism: a tool for automatic verification of probabilistic systems. In: Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 441–444
23.
Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Computer aided verification. Springer, Berlin, pp 154–169
24.
Chen T, Diciolla M, Kwiatkowska M, Mereacre A (2013) Verification of linear duration properties over continuous-time markov chains. ACM Trans Comput Logic: TOCL 14(4):33MathSciNetCrossRefMATH
25.
Kwiatkowska M, Norman G, Parker D (2007) Stochastic model checking. In: Formal methods for performance evaluation. Springer, Berlin, pp 220–270
Metadaten
Titel
Formal verification of SysML diagram using case studies of real-time system
verfasst von
Sajjad Ali
Publikationsdatum
22.12.2018
Verlag
Springer London
Erschienen in
Innovations in Systems and Software Engineering / Ausgabe 4/2018
Print ISSN: 1614-5046
Elektronische ISSN: 1614-5054
DOI
https://doi.org/10.1007/s11334-018-0318-5

Premium Partner

    Bildnachweise