Formal methods encompass a wide choice of techniques and tools for the specification, development, analysis, and verification of software and hardware systems. Formal methods are widely applied in industry, in activities ranging from the elicitation of requirements and the early design phases all the way to the deployment, configuration, and runtime monitoring of actual systems. Formal methods allow one to precisely specify the environment in which a system operates, the requirements and properties that the system should satisfy, the models of the system used during the various design steps, and the code embedded in the final implementation, as well as to express conformance relations between these specifications. We present a broad scope of successful applications of formal methods in industry, not limited to the well-known success stories from the safety-critical domain, like railways and other transportation systems, but also covering other areas such as lithography manufacturing and cloud security in e-commerce, to name but a few. We also report testimonies from a number of representatives from industry who, either directly or indirectly, use or have used formal methods in their industrial project endeavours. These persons are spread geographically, including Europe, Asia, North and South America, and the involved projects witness the large coverage of applications of formal methods, not limited to the safety-critical domain. We thus make a case for the importance of formal methods, and in particular of the capacity to abstract and mathematical reasoning that are taught as part of any formal methods course. These are fundamental Computer Science skills that graduates should profit from when working as computer scientists in industry, as confirmed by industry representatives.

The study of cardiac arrhythmias has spurred the development of models across a variety of formulations and scales and designed for different purposes, each with distinct configuration spaces. Nevertheless, these models should be able to exhibit equivalent behavior when their contexts overlap. Configuring models to both support this context equivalence and still exhibit intended behavioral characteristics can be challenging. Due to the complexity of this problem, automation can be desirable. We present a framework aimed at automating the comprehension and alignment of cardiac model behaviors. For model comprehension, we mine a set of properties (invariants) that a model with given configuration will exhibit when executed. Comprehension can be extended to model alignment: we perform comprehension of one model, and then mine a set of configurations for a second, each of which produces invariants aligned to the invariants of the first. The configuration spaces of the two models under study need not be related in any way; rather, the systems are compared by means of the system invariants that they each exhibit. We model system invariants as association rules, a well-studied representation used in the field of data mining. We apply our methodology to two one-dimensional models of cardiac tissue. One model is the well-known differential-equations-based Fenton-Karma model representing the electrophysiology of interconnected cardiac cells, while the other is a timed automaton representation of cardiac tissue designed to enable formal analysis. We demonstrate alignment of the models with respect to activation rates and path conductance. We expect this methodology can be generalized beyond cardiac models.

This report contains the descriptions of the timed automata (models) and the properties (specifications) that are used as the "benchmark examples in Data structure choices for on-the-fly model checking of real-time systems" and "The power of proofs: New algorithms for timed automata model checking." The four models from those sources are: CSMA, FISCHER, LEADER, and GRC. Additionally we include in this report two additional models: FDDI and PATHOS. These six models are often used to benchmark timed automata model checker speed throughout timed automata model checking papers.

Using a probabilistic reachability-based approach, we present a multi-parameter bifurcation analysis of electrical alternans in the two-current Mitchell–Schaeffer (MS) cardiac-cell model. Electrical alternans is a phenomenon characterized by a variation in successive Action Potential Durations generated by a cardiac cell or tissue. Alternans are known to initiate re-entrant waves and are an important physiological indicator of an impending life-threatening arrhythmia such as ventricular fibrillation. The multi-parameter bifurcation analysis we perform identifies a bifurcation hypersurface in the MS model parameter space, such that a small perturbation to this region results in a transition from highly likely alternans to highly likely non-alternans behavior. Our approach to this problem rests on encoding alternans-like behavior in the MS model as a five-mode, multinomial hybrid automaton. To perform multi-parameter bifurcation analysis of cardiac alternans, we first treat the parameters in question as bounded random variables. We then apply a sophisticated guided-search-based probabilistic reachability analysis to compute a bounded bifurcation region (possibly very tight) that contains the bifurcation hypersurface (BH). Our probabilistic reachability analysis uses a technique that combines a δ -decision procedure with statistical tests. In the process of computing the bifurcation region, we further partition the parameter space into two more regions such that any valuation chosen from one of the regions will either produce alternans or non-alternans behavior with a probability greater than a user-defined threshold.

Scott Smolka and I have been colleagues for over 30 years. In this note I reminisce about our history as collaborators, colleagues and friends.

This note corrects a technical error in the ACM Computing Surveys article mentioned in the title. The flaw involved constructions for showing that timed automata with urgent locations have the same expressiveness as timed automata that allow false location invariants. Corrected constructions are presented in this note, and the affected results are reproved.

The query-checking problem for temporal logic may be formulated as follows. Given a Kripke structure M and a temporal-logic query of form \(\phi \left[ {\texttt {var}}\right] \), which may be thought of as a temporal formula with a missing propositional subformula \({\texttt {var}}\), find the most precise propositional formula f that, when substituted for \({\texttt {var}}\) in \(\phi \left[ {\texttt {var}}\right] \), ensures M satisfies the resulting temporal property. Query checking has been used for system comprehension, specification reconstruction, and other related applications in the formal analysis of systems.

In this work, we develop a generalization of Hennessy-Milner Logic (HML) for Generalized Synchronization Trees (GSTs) that we call Generalized Hennessy Milner Logic (GHML). Importantly, this logic suggests a strong relationship between (weak) bisimulation for GSTs and ordinary bisimulation for Synchronization Trees (STs). We demonstrate that this relationship can be used to define the GST analog for image-finiteness of STs. Furthermore, we demonstrate that certain maximal Hennessy-Milner classes of STs have counterparts in maximal Hennessy-Milner classes of GSTs with respect to GST weak bisimulation. We also exhibit some interesting characteristics of these maximal Hennessy-Milner classes of GSTs.

This note corrects a technical error in the ACM Computing Surveys article mentioned in the title. The flaw involved constructions for showing that timed automata with urgent locations have the same expressiveness as timed automata that allow false location invariants. Corrected constructions are presented in this note, and the affected results are reproved.

This paper presents an operational semantics for UML activity diagrams. The purpose of this semantics is three-fold: to give a robust basis for verifying model correctness; to help validate model transformations; and to provide a well-formed basis for assessing whether a proposed extension/interpretation of the modeling language is consistent with the standard. The challenges of a general formal framework for UML models include the semi-formality of the semantics specification, the extensibility of the language, and (sometimes deliberate, sometimes accidental) under-specification of model behavior in the standard. Our approach is based on structural operational semantics, which can be extended according to domain-specific needs. The presented semantics has been implemented and tested.

In this paper, we survey recent progress in CyberCardia project, a CPS Frontier project funded by the National Science Foundation. The CyberCardia project will lead to significant advances in the state of the art for system verification and cardiac therapies based on the use of formal methods and closed-loop control and verification. The animating vision for the work is to enable the development of a true in silico design methodology for medical devices that can be used to speed the development of new devices and to provide greater assurance that their behavior matches designer intentions, and to pass regulatory muster more quickly so that they can be used on patients needing their care.The acceleration in medical-device innovation achievable as a result of the CyberCardia research will also have long-term and sustained societal benefits, as better diagnostic and therapeutic technologies enter into the practice of medicine more quickly.

We present a bifurcation analysis of electrical alternans in the two-current Mitchell-Schaeffer (MS) cardiac-cell model using the theory of δ-decidability over the reals. Electrical alternans is a phenomenon characterized by a variation in the successive Action Potential Durations (APDs) generated by a single cardiac cell or tissue. Alternans are known to initiate re-entrant waves and are an important physiological indicator of an impending life-threatening arrhythmia such as ventricular fibrillation. The bifurcation analysis we perform determines, for each control parameter τ of the MS model, the bifurcation point in the range of τ such that a small perturbation to this value results in a transition from alternans to non-alternans behavior. To the best of our knowledge, our analysis represents the first formal verification of non-trivial dynamics in a numerical cardiac-cell model. Our approach to this problem rests on encoding alternans-like behavior in the MS model as a 11-mode, multinomial hybrid automaton (HA). For each model parameter, we then apply a sophisticated, guided-searchbased reachability analysis to this HA to estimate parameter ranges for both alternans and non-alternans behavior. The bifurcation point separates these two ranges, but with an uncertainty region due to the underlying δ-decision procedure. This uncertainty region, however, can be reduced by decreasing δ at the expense of increasing the model exploration time. Experimental results are provided that highlight the effectiveness of this method.

Many systems make use of concurrent tasks, however it is often difficult to test concurrent design. Therefore, many test cases are simplified and do not fully test all concurrency aspects of the system. We encountered this problem when analyzing test cases for concurrent flight software at NASA. To address this problem, we developed and evaluated a model based testing (MBT) technique for testing of concurrent systems. Using MBT, the tester creates a model, which is based on the requirements of the system under test (SUT), and lets the computer generate innumerable test cases automatically from the model. We evaluate the effectiveness of the technique using Microsoft's Spec Explorer MBT tool. We apply the technique on NASA's Core Flight Software (cFS) software bus module API, which is based on a concurrent publisher-subscriber architecture style and is a safety-critical system. We describe how we created a test automation architecture for testing concurrent inter-task communication as carried out by the software bus. We also investigate the type of issues the technique for testing of concurrent systems can find as well as what degree of code coverage it can achieve.

We present a framework for opacity in cyberphysical systems modeled as discrete time linear time invariant systems. A set of secret states is k - ISO with respect to a set of nonsecret states if, starting from these sets at time 0, the outputs at time k are indistinguishable to a passive adversarial observer. Necessary and sufficient conditions for k - ISO are given in terms of reachable sets of the system. Properties of k - ISO under unions and intersections are verified. It is seen that while unions of opaque sets preserve opacity, this is not necessarily true for intersections. We show that under certain conditions, k - ISO is equivalent to output controllability. Finally, we present an algorithm to compute a k - ISO set of states, given candidate secret and nonsecret sets of initial states.

With cybersecurity increasingly becoming a focus of regulatory concern, both medical device manufacturers and regulators are facing another challenge: how to establish, and also demonstrate, that the devices are also secure. This paper outlines an approach to constructing assurance cases to capture assumptions about the attacker by 1) identifying the hazards of interest to attacker; 2) identifying attack surfaces; 3) enumerating vulnerabilities and attack scenarios; and 4) ranking attack scenarios on the basis of a risk model. Introducing the security considerations early in the design cycle, we can better integrate security with existing engineering processes to yield documents that both improve the engineering processes and are acceptable for regulatory oversight.

This paper introduces a translation tool that supports formal verification of UML activity diagrams using the model checkers: UPPAAL, SPIN, NuSMV and PES. The motivation for this tool arises from the desire to check the properties of a system early in the development process, and the fact that UML is commonly used to describe software models. The tool is implemented as an Eclipse-plugin that automatically translates the UML activities and logical requirements into valid input notation for the model checkers. The automated aspect of the plugin allows users without a background in formal methods to verify the safety and liveness of a system. The translation strategies implemented in this plugin are the result of an experimental study. A tutorial video can be found in https://www.youtube.com/watch?v=AHsih8REUxM.

We compare manual testing without any automation performed by a tester at a software company with model-based testing (MBT) performed by a tester at a research center. The system under test (SUT), of which two different versions were tested by each of the two testers, is a professionally developed web-based data collection system that now is in use. The two testers tested the same versions, had identical testing goals (to detect defects), had access to the same resources, but used different processes (i.e. manual without any automation vs. model-based with automatic test case generation and automatic test case execution). The testers did not interact with each other. We compare the effectiveness (issues found) and efficiency (effort spent) of the two approaches. The results show, for example, that manual testing required less preparation time and that its test coverage was somewhat uneven. In contrast, MBT required more preparation time, was more systematic, and detected more issues. While the manual approach detected more inconsistencies between specified and actual text labels, MBT detected more functional issues. This is reflected in the severity score summary which was about 60% higher for MBT than Manual.

This paper is a proposal for a poster. In it we describe a medical device security approach that researchers at Fraunhofer used to analyze different kinds of medical devices for security vulnerabilities. These medical devices were provided to Fraunhofer by a medical device manufacturer whose name we cannot disclose due to non-disclosure agreements.

This paper presents the first model-checking algorithm for an expressive modal mu-calculus over timed automata, \(L^{\mathit{rel}, \mathit{af}}_{\nu,\mu}\), and reports performance results for an implementation. This mu-calculus contains extended time-modality operators and can express all of TCTL. Our algorithmic approach uses an “on-the-fly” strategy based on proof search as a means of ensuring high performance for both positive and negative answers to model-checking questions. In particular, a set of proof rules for solving model-checking problems are given and proved sound and complete; our algorithm then model-checks a property by constructing a proof (or showing none exists) using these rules. One noteworthy aspect of our technique is that we show that verification performance can be improved with derived rules, whose correctness can be inferred from the more primitive rules on which they are based. In this paper, we give the basic proof rules underlying our method, describe derived proof rules to improve performance, and we compare our implementation to UPPAAL.