Upgradation of Programmable Logic Controller (PLC) software is quite common to accommodate evolving industrial requirements. Verifying the correctness of such upgrades remains a significant challenge. In this paper, we propose a verification-based approach to ensure the correctness of the existing functionality in the upgraded version of a PLC software. The method converts the older and the newer versions of the sequential function chart (SFC) into two Petri net models. We then verify whether one model is contained within another, based on a novel containment checking algorithm grounded in symbolic path equivalence. For this purpose, we have developed a home-grown Petri net-based containment checker. Experimental evaluation on 80 real-world benchmarks from the OSCAT library highlights the scalability and effectiveness of the framework. We have compared our approach with verifAPS, a popular tool used for software upgradation, and observed nearly 4x performance improvement.
We present ERODE, a tool introduced in 2016 to analyze and reduce differential equations and chemical reaction networks. Over the years, it has been extended with further analysis and reduction techniques, as well as formalisms including differential algebraic equations, Boolean networks, networks, and Markov chains. ERODE can importexport towards several tools, including Matlab, BioNetGen, Modelica, PRISM, STORM, Stochkit, GINsim, SBML, and CoLoMoTo. It also has Python APIs.
This paper deals with the problem of runtime enforcement (RE) in the context of reactive systems, which consists in modifying the outputs of a system minimally to ensure its correctness. In contrast to enforcers that can postpone events via buffering, enforcers for reactive systems must operate within the same reactive cycle, always yielding a (possibly modified) output. For safety properties, an enforcer makes sure to satisfy the property at each step. However, for general regular properties, one can only expect to satisfy the property eventually. There is then a risk that even under enforcement the satisfaction is indefinitely delayed, and the property is never actually satisfied. Forcing the satisfaction of regular or ω -regular properties has been considered using bounded fairness and prompt eventuality. In this paper, we propose a new runtime enforcement framework for regular properties with prompt eventualities. Given an automaton specifying a property φ and a bound k, the enforcer should never falsify φ more than k consecutive steps. We formally define this RE problem, characterize k-enforceability of automata, and exhibit the construction of the enforcer. Rather than fixing k, we also study whether k can be computed to ensure k-enforceability or some maximal coverage of φ . We implement the k-prompt enforcement framework, and demonstrate its behaviour with varying k.
In this paper we tackle the problem of proving generic LTL properties of hybrid systems with a particular focus on liveness properties such as recurrence of regions, response to stimuli, or region stability. Although many advances have been made in the analysis of reachability and safety properties of dynamic and hybrid systems, there is a lack of tool support for the automated verification of liveness properties. We propose a fully automated approach that combines Lyapunov synthesis, reachability analysis, and SMT-based quantifier elimination to build a discrete abstraction and then applies standard model checking algorithms. A key step of the algorithm is the derivation of LTL constraints from reachable sets computations and Lyapunov-like certificates. We implemented the approach on top of the CORA and nuXmv tools and show how it can scale in the size of the discrete structure and how it can prove properties over linear and non-linear complex dynamics.
