[Zurück]


Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):

R. Hoch, H. Kaindl:
"Verification of Feature Coordination using the Fluent Calculus [Best Paper Nomination]";
Vortrag: ENASE 2018, Funchal, Madeira, Portugal; 23.03.2018 - 24.03.2018; in: "Proceedings of the 13th International Conference on Evaluation of Novel Approaches to Software Engineering - Volume 1: ENASE", INSTICC (Hrg.); SciTePress, Volume 1 (2018), ISBN: 978-989-758-300-1; S. 169 - 179.



Kurzfassung englisch:
Previously, an approach based on the Situation Calculus was published for specifying feature coordination
of a software system, but without a physical model or any additional autonomous agent in the environment.
Hence, no verification of the feature coordination was possible in spite of its formal specification. Verification
of safety-critical feature coordination is important, however, and requires additional models. This paper shows
that a specification of a software coordinator can be formally verified using the Fluent Calculus (a derivative
of the Situation Calculus), when combined with additional models. The overall qualitative model is a reimplementation
of a recently published one based on synchronized finite-state machines, which was used for
model checking. In fact, we show how the model in Fluent Calculus can be systematically derived from the
finite-state machines. The results of verification using the Fluent Calculus correspond to those using model
checking. We also contrast our approach using the Fluent Calculus with model checking. In summary, we
present verification of (safety-critical) feature coordination using the Fluent Calculus.

Schlagworte:
Verification, Fluent Calculus, Situation Calculus, Model Checking


"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.5220/0006771401690179


Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.