Towards Building Verifiable CPS using Lingua Franca*

Shaokai Lin, Yatin A. Manerkar, Marten Lohstroh, Elizabeth Polgreen, Sheng-Jung Yu, Chadlia Jerad, Edward A. Lee, Sanjit A. Seshia

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

Formal verification of cyber-physical systems (CPS) is challenging because it has to consider real-time and concurrency aspects that are often absent in ordinary software. Moreover, the software in CPS is often complex and low-level, making it hard to assure that a formal model of the system used for verification is a faithful representation of the actual implementation, which can undermine the value of a verification result. To address this problem, we propose a methodology for building verifiable CPS based on the principle that a formal model of the software can be derived automatically from its implementation. Our approach requires that the system implementation is specified in Lingua Franca (LF), a polyglot coordination language tailored for real-time, concurrent CPS, which we made amenable to the specification of safety properties via annotations in the code. The program structure and the deterministic semantics of LF enable automatic construction of formal axiomatic models directly from LF programs. The generated models are automatically checked using Bounded Model Checking (BMC) by the verification engine Uclid5 using the Z3 SMT solver. The proposed technique enables checking a well-defined fragment of Safety Metric Temporal Logic (Safety MTL) formulas. To ensure the completeness of BMC, we present a method to derive an upper bound on the completeness threshold of an axiomatic model based on the semantics of LF. We implement our approach in the LF Verifier and evaluate it using a benchmark suite with 22 programs sampled from real-life applications and benchmarks for Erlang, Lustre, actor-oriented languages, and RTOSes. The LF Verifier correctly checks 21 out of 22 programs automatically
Original languageEnglish
Article number155
Pages (from-to)1-24
Number of pages24
JournalACM Transactions on Embedded Computing Systems
Volume22
Issue number5
DOIs
Publication statusPublished - 9 Sept 2023
EventEMSOFT 2023: International Conference on Embedded Software - Hamburg, Germany
Duration: 17 Sept 202322 Sept 2023
https://esweek.org/emsoft/

Keywords / Materials (for Non-textual outputs)

  • cyber-physical systems
  • concurrency
  • safety MTL
  • axiomatic modeling
  • automated verfication
  • model-based design

Fingerprint

Dive into the research topics of 'Towards Building Verifiable CPS using Lingua Franca*'. Together they form a unique fingerprint.

Cite this