LF-mc: An Efficient Verifier for Lingua Franca
Mario Reja, Mikheil Rukhaia, Kyungmin Bae, Mircea Marin, Peter Csaba Ölveczky
This tool paper presents the LF-mc verification tool for the Lingua Franca (LF) coordination language for cyber-physical systems. LF-mc is the only verification tool which is based on LF’s logical-time semantics, and therefore gives correct analysis results. LF-mc is also the only verifier for LF that supports a model of nondeterministic environments (“physical actions”). LF-mc is fully integrated into the LF toolchain, and provides system simulation as well as fully automatic unbounded and time-bounded reachability analysis and LTL model checking for both state-based and action-based properties. Extensive benchmarking shows that LF-mc significantly outperforms the LF Verifier and PolyVer analysis tools for LF.