Temporal Logics Meet Real-World Software Requirements: A Reality Check
This program is tentative and subject to change.
Reasoning on the behavior of software systems is challenging, especially in critical domains such as aerospace. Transitioning from natural language to formal specifications enables long-pursued activities such as modeling, synthesis, and verification. Temporal logics are often used in this regard, each with different operators, expressiveness or associated implementations. However, a significant gap exists between the theoretical capabilities of the logics applied in formal methods and the practical needs for specifying real-world requirements. This paper addresses this gap through a case study of SpaceWire, a standard specification for a data-handling communication protocol often adopted on spacecraft and other on-board systems. We extract 89 software requirements exhibiting temporal behavior and transcribe them into logic-based formalizations using different established temporal logics, maximizing natural encoding. We analyze the suitability of the chosen logics for formalizing the selected software requirements to reason about potential implications for both researchers and practitioners.
This program is tentative and subject to change.
Sun 27 AprDisplayed time zone: Eastern Time (US & Canada) change
16:00 - 17:30 | |||
16:00 30mTalk | Specifying Distributed Hash Tables with Allen Temporal Logic Research Track Nuno Policarpo Instituto Superior Técnico, University of Lisbon, José Fragoso Santos INESC-ID/Instituto Superior Técnico, Portugal , Alcino Cunha University of Minho; INESC TEC, João Leitão NOVA LINCS & FCT, NOVA University of Lisbon, Pedro Ákos Costa NOVA LINCS & DI-FCT-UNL | ||
16:30 30mTalk | Temporal Logics Meet Real-World Software Requirements: A Reality Check Research Track Roman Bögli University of Bern, Atefeh Rohani University of Bern, Thomas Studer University of Bern, Christos Tsigkanos University of Athens, Greece, Timo Kehrer University of Bern | ||
17:00 30mTalk | Detecting Redundant Preconditions Research Track Nicola Thoben University of Oldenburg, Heike Wehrheim Carl von Ossietzky Universität Oldenburg / University of Oldenburg |