Abstract : We present a method and tools for formally modelling software using
finite-state machines, where transitions are labelled with predicates instead of events. We review the scheduling of an arrangement of
logically labelled finite state machines (LLFSMs) and show the
extension of the formally defined semantics of LLFSMs to multi-threaded and concurrent systems. We show we can build model-to-text transformations from the model of a system into assembly language, high-level languages, and the input of two model checkers (NuSMV and TLC). Our translations have no semantic gaps, ensuring verification with both model-checkers match the executable version.
Moreover, for the first time, we provide a formal translation of LLFSM into  TLAp and show that our model checker simulations, applied to our translations to NuSMV, match the execution of our translation to C or MIPS. We illustrate the benefits of our method with several well-studied examples, such as a microwave with real-time constraints,  Fischer's mutual exclusion algorithm (for multi-threaded systems and concurrency control), the two-phase commit protocol (for distributed consensus), and a three-floor elevator (used for verification of descriptions using the  IEC~61499 standard). We show examples of applying these tools and methods to embedded systems and robotic systems, and we point out how we produce deliberative architectures with logic languages like Prolog or some Propositional Plausible Logics.


Until recently, Vladimir Estivill-Castro was the dean of the Department of Engineering at Universitat Pompeu Fabra in Barcelona, Spain. His work in machine ethics earned him an invitation to the EU Committee for 'Guidelines for the Responsible Use of Generative AI,' he is a principal investigator for AI-Boost, focusing on trustworthy and explainable AI. He leads MI-PAL, which has participated in eight editions of the Standard Platform League using the Humanoid Robot Nao. His main interests include software engineering for embedded and robotic systems, algorithmic engineering, computational complexity, intelligent data analysis, and privacy-preserving data mining. He also explores algorithmic game theory, modelling behaviour for model-driven development, and formal methods in software engineering. Prof. Estivill-Castro holds a PhD from the University of Waterloo in Canada and has received the best supervision award in 2010 from the Australian Teaching and Learning Council.