Talk "Semantics and Formal Analysis of Lingua Franca CPS Specifications in Rewriting Logic"

by Peter Ölveczky

Sat, 02 November 2024 at 04:30 pm in Crete, Greece

Joint work with: Mircea Marin, Mario Reja, Mikheil Rukhaia, and Kyungmin Bae

Abstract: In this paper we formalize in rewriting logic the intended discrete-event semantics of the recent Lingua Franca coordination language for cyber-physical systems. We then show how Lingua Franca models can be simulated and model checked using Maude, and provide functionality that should make the formal analysis easy to perform also for the Maude non-expert. We illustrate such Maude verification on a number of existing Lingua Franca models, including of a car driver assistance system and of train door controllers. To the best of our knowledge, this is the first verification framework for Lingua Franca that captures the intended semantics of the language, and which therefore provides correct (and state-space efficient) model checking analysis for Lingua Franca.