Logo des Repositoriums

Auflistung nach Schlagwort "Formal methods"

1 - 2 von 2
  • ConferencePaper
    Skill-Based Verification of Cyber-Physical Systems
    (Software Engineering 2021, 2021) Knüppel, Alexander; Jatzkowski, Inga; Nolte, Marcus; Runge, Tobias; Thüm, Thomas; Schaefer, Ina
    This work has been accepted at the 23rd International Conference on Fundamental Approaches to Software Engineering, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020. The increase of complexity in modeling cyber-physical systems poses a challenge for formally ensuring their functional correctness. Lack of expert knowledge and scalability are two limiting factors that prohibit a seamless integration into today's software engineering processes. To address this challenge, we propose to adopt and formalize the notion of skill graphs, an abstract and easy-to-use modeling notion for representing automated vehicle driving maneuvers. For formally verifying that skill graphs are well-formed and comply with a given set of safety requirements, we incorporate hybrid programs into our formalization. Hybrid programs constitute a program notion for cyber-physical systems on the basis of differential dynamic logic, which enables deductive and compositional verification following the idea of Hoare-style reasoning. That is, simpler verified skill graphs can be combined to exhibit complex maneuvers while validity is retained (i.e., without the need of re-verification). To showcase the benefits of our theoretical considerations, we implemented our framework in an open-source tool named Skeditor and conducted a case study exhibiting an automatic vehicle follow mode.
  • Zeitschriftenartikel
    Verifikation von Webservicekompositionen:
    (Wirtschaftsinformatik: Vol. 51, No. 6, 2009) Röglinger, Maximilian
    Webservicekompositionen koordinieren Webservices verschiedener Unternehmen. Es wird erwartet, dass sie die Grundlage serviceorientierter Architekturen bilden, Geschäftsprozesse verbessern sowie zur Förderung intra- und interorganisatorischer Integration beitragen. Vor allem in interorganisatorischen Kontexten stellen die Dienstqualität bezogen auf nichtfunktionale Anforderungen und die Konformität mit funktionalen Anforderungen zunehmend wichtige Merkmale dar. Da Webservicekompositionen asynchrone und verteilte Systeme sind, kann die zweite – auch als Korrektheit bezeichnete – Eigenschaft am besten mittels Verifikation nachgewiesen werden. Dieser Beitrag untersucht aus systemtheoretischer Perspektive, wie der Korrektheitsbegriff für Webservicekompositionen konkretisiert werden kann. Außerdem wird ein Anforderungsframework für serviceorientierte Modellierungsansätze vorgeschlagen, sodass Korrektheit durch Verifikation gezeigt werden kann und Webservicekompositionen intuitiv modelliert werden können. Um die prinzipielle Anwendbarkeit des Frameworks zu demonstrieren, wird ein beispielhafter Ansatz in Bezug auf die Anforderungen des Frameworks analysiert.AbstractWeb service compositions coordinate Web services of different enterprises. They are expected to constitute the foundation of service-oriented architectures, to improve business processes as well as to foster intra- and inter-organizational integration. Especially in inter-organizational contexts, quality of service referring to non-functional requirements and conformance to functional requirements are becoming vital properties. With Web service compositions being asynchronous and distributed systems, the latter property – which is also called correctness – can be shown best by verification. This paper examines from a system-theoretic perspective how correctness can be operationalized for Web service compositions. It also proposes a requirements framework for service-oriented modeling techniques so that correctness can be shown by verification and Web service compositions can be modeled intuitively. In order to show the framework’s principle applicability, an example approach is analyzed with respect to the corresponding requirements.