CMACS/AVACS Workshop & PI Meeting

Hosted by Carnegie Mellon University, Pittsburgh, PA. Wed-Fri Nov. 20-22, 2013.

 

Wednesday, Nov. 20, 2013: CMACS PI Mtg
8:30	Breakfast
9:30	Opening remarks for PI Mtg
10:00	Natasa Miskov-Zivanov, "Formal modeling and analysis of timing in biological networks: application to cellular decisions in the immune system" PDF
10:45	James Glimm, "Resolution Enhanced Electro-Cardiac Simulations" PPT
11:30	Coffee Break
11:45	Peter Fontana, "The Power of Proofs: New Algorithms for Timed Automata Model Checking" PDF
12:15	Lunch
1:30	Sarah Loos, "Teaching and Proving CPS" PDF
2:15	Anvesh Komuravelli, "The SPACER framework -- Automatic Abstractions from Proofs and Counterexamples" PPT
3:30	Break
4:00	Discussion on future plans
5:30	End of session
Thursday, Nov 21, 2013: CMACS/AVACS Workshop
8:15	Breakfast
8:30	Werner Damm, "Overview of AVACS." PDF
9:00	Christoph Scholl, "Verification of linear hybrid systems: Symbolic representations using simple interpolants." PDF
10:00	Bernd Finkbeiner, "Synthesis of Observation Predicates" PDF
11:00	Bing Liu, "Parameter identification using delta-decisions for hybrid systems in biology" PDF
11:30	Stefan Mitsch, "Provably Safe Obstacle Avoidance of Autonomous Robotic Ground Vehicles" PDF
12:00	Lunch
1:00	Flavio Fenton, "Highlights from CMACS Workshops" PDF, and "Near-real-time interactive simulations of complex cardiac cell models in tissue over the web on desktops, laptops and cell phones"
1:30	Zamira Daw, "Integrating model checking and UML based model-driven development for embedded systems" PDF
2:00	Khalil Ghorbal, "Abstracting Algebraic Differential Equations by Differential Radical Invariants" PDF
2:30	Radu Grosu, "Compositionality Results for Cardiac Cell Dynamics" PDF
3:15	Break
3:30	Andre Platzer, "Logic of Hybrid Games." PDF
4:15	Werner Damm, "Does it pay to extend the perimeter of a world model." PDF
5:00	Discussion
6:00	End of Session
Friday, Nov 22, 2013
8:30	Breakfast
9:00	Andreas Podelski, "Proofs that count"
9:45	Christoph Weidenbach, "Beyond SAT and SMT: Automated Reasoning Building Blocks" PDF
10:30	Break
10:45	Sicun Gao, "Models, Decisions, and Better Cyber-Physical Systems."
11:15	Soonho Kong, "The dReal/dReach Solver." PDF / WWW / Tools
11:45	Lunch
1:00	Thomas Wies, "Automated Debugging with Error Invariants" PDF
1:45	Ruzica Piskac, "Type Inhabitation Problem for Code Completion and Repair" PDF
2:30	Nikos Archega, "Hybrid invariants for theorem provers"
3:00	End of Program

Talk titles & abstracts

Nikos Arechiga - "Hybrid invariants for theorem provers"

Verifying the safety of hybrid dynamical systems is a difficult problem. This paper presents a deductive method that facilitates the process of developing a proof of system safety with the help of a semi-interactive theorem prover. Designers can often use established numerical methods to derive safety certificates such as forward invariant sets, barrier certificates, and reachable state sets for behaviors associated with individual modes. Our technique allows the user to take advantage of this by locally reasoning about behaviors in various modes and lazily discovering mode-specific invariants as required at each stage of the proof. Our key contribution is a new inference rule, the {\em hybrid cut rule} introduced into the proof calculus of the theorem prover KeYmaera. KeYmaera uses this rule to excise parts of the hybrid state space for which the user can supply local safety certificates from the overall safety proof, leaving it with a smaller sub-goal. We demonstrate the cut rule in action on an academic example, and use it to prove safety of two representative automotive powertrain control systems.

Werner Damm - "Does it pay to extend the perimeter of a world model" PDF

Will the cost for observing additional real-world phenomena in a world model be recovered by the resulting increase in the quality of the implementations based on the model? We address the quest for optimal models in light of industrial practices in systems engineering, where the development of control strategies is based on combined models of a system and its environment. We introduce the notion of remorsefree dominance between strategies, where one strategy is preferred over another if it outperforms the other strategy in comparable situations, even if neither strategy is guaranteed to achieve all objectives. We call a world model optimal if it is sufficiently precise to allow for a remorsefree dominating strategy that is guaranteed to remain dominant even if the world model is refined. We present algorithms for the automatic verification and synthesis of dominant strategies, based on tree automata constructions from reactive synthesis.

Zamira Daw - "Integrating model checking and UML based model-driven development for embedded systems" PDF

Integration of model checking into model-driven development allows system’s verification in early phases of the development. Furthermore it facilitates the use of formal methods by programmers, which often have more confidence with development models like UML but usually no background in formal techniques. In this talk, we will present relevant aspects to the integration of model checkers into a UML model-based development environment for the verification of embedded systems. The environment, DMOSES, is based on a formalization of UML Activity Diagrams and is used to generate correct and efficient code from such models; a key application area is the medical-device domain. The introduction of formal verification into the model-driven development process allows the assessment of the correctness of design models before they are used to generate source code. We will demonstrate the verification of system requirements with a case study of an infusion pump and discuss some of the issues of integrating model checkers into the DMOSES process. The case study also contains a performance evaluation of two different model checkers: NuSMV and UPPAAL

Flavio Fenton - "Near-real-time interactive simulations of complex cardiac cell models in tissue over the web on desktops, laptops and cell phones"

Introduction: Over the past decades a large number of cardiac cell models have been developed. However, their complexity and many variables have restricted simulation studies in tissue to supercomputers and a handful of research labs.

Methods: Graphics processing units (GPUs) now standard in most devices contain multiprocessors allowing parallelization and effectively act as personal supercomputers. The programming interface WebGL allows direct GPU access through a web-browser that therefore is independent of the architecture and operating system. Within this framework we have coded cardiac cell models from the 8-variable Beeler-Reuter and Luo-Rudy to the 13-variable Fox et al. and 19-variable Ten-Tusscher et al. ventricular models and 29-variable Nygren et al. atrial cell model among others.

Results: These models can be accessed via the web and run on any device with a GPU. Users can simulate any of these models on a 2D tissue of 13x13cm^2 and change parameters on the fly to visualize and study the dynamics of the AP waves as a function of the various model parameters. In addition by clicking on the screen the user can inject current and elicit activations anytime and anywhere to study reentry induction and set a pacing site and frequency to visualize and study concordant and discordant alternans.

Conclusions: Simulation of complex cell models for study or demonstrations are accessible for the first time by anyone, from clinicians, researchers, and students to patients, at speeds comparable to those of supercomputers but on a laptop or a cell phone.

Bernd Finkbeiner - "Synthesis of Observation Predicates" PDF

We present a novel approach to the safety controller synthesis problem with partial observability for real-time systems. This in general undecidable problem can be reduced to a decidable one by fixing the granularity of the controller: finite sets of clocks and constants in the guards. Current state-of-the-art methods are limited to brute-force enumeration of possible granularities or manual choice of a finite set of observations that a controller can track. We address this limitation by proposing a counterexample-guided method to successively refine a set of observations until a sufficiently precise abstraction is obtained. The size of the abstract games and strategies generated by our approach depends on the number of observation predicates and not on the size of the constants in the plant. The talk is based on joint work with Rayna Dimitrova.

Peter Fontana - "The Power of Proofs: New Algorithms for Timed Automata Model Checking" PDF

This paper presents a new model-checking algorithm for an expressive modal mu-calculus over timed automata 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; answering a model-checking question amounts to building a proof (or showing none exists) using the rules. One noteworthy aspect of our technique is that we show that verification performance can be improved with \emph{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 report on our implementation of this model checker and its comparison to the UPPAAL tool.

Sicun Gao - "Models, Decisions, and Better Cyber-Physical Systems."

The analysis and design of reliable Cyber-Physical Systems naturally require extensions of all existing techniques for dealing with discrete and continuous systems, but success has been limited by a lack of unifying methodology. To change the situation, we are developing theories and tools for a new model-based design framework for CPS that combines verification, synthesis, and reliable code-generation. At the core of the framework is our recent breakthroughs in the bottleneck problem of solving nonlinear logical constraints over Euclidean spaces. I will survey some of our results and on-going projects, such as delta-decidability over the reals, SMT with differential equations, the dReal/dReach solver, and applications in realistic systems from automotive, robotics, and medical applications.

Khalil Ghorbal - "Abstracting Algebraic Differential Equations by Differential Radical Invariants" PDF

Reasoning about the solutions of differential equations by means of their first integrals (conserved functions and expressions) is ubiquitous all over science studying dynamical processes. In computer science, the interest of the automated generation of algebraic invariants was essentially driven and motivated by the formal verification of different aspects of hybrid systems, i.e. systems combining discrete dynamics with differential equations for the continuous dynamics.

In this talk, we present a necessary and sufficient characterization of algebraic invariants of algebraic differential equations by a differential radical invariance criterion, i.e. an explicit equation on higher-order Lie derivatives. Differential radical invariants are computationally easy to check using polynomial arithmetic on higher-order Lie derivatives. The characterization makes it possible to generate invariants by solving for the coefficients in a parametrization by comparing coefficients.

James Glimm - "Resolution Enhanced Electro-Cardiac Simulations" PPT

We propose improve simulation capabilities of some common electro-cardiac simulation models, in three basic directions. Work in progress is directed to the following goals:

(1) We introduce higher order sharp boundary methods into the solution of the diffusion step for the electrical voltages. This allows increased resolution and accuracy, in removing surface or boundary artifacts from simulations.

(2) We solve the diffusion step implicitly, allowing larger time steps (limited only by solution accuracy and not by numerical stability).

(3) We extend mono-domain models to a bidomain model, which describes separately the voltages within and between the cardiac cells. This later step is important in modeling of defibrillators, whose voltage is normally deposited in the extracellular system, and which then couples to the cardiac cells themselves for the purpose of defibrillation.

Radu Grosu - "Compositionality Results for Cardiac Cell Dynamics" PDF

By appealing to the small-gain theorem of one of the au- thors (Girard), we show that the 13-variable sodium-channel component of the IMW cardiac-cell model (Iyer-Mazhari-Winslow) can be replaced by an approximately bisimilar, 2- variable HH-type (Hodgkin-Huxley) abstraction. We show that this substitution of (approximately) equals for equals is safe in the sense that the approximation error between sodium-channel models does not get ampli ed by the feed- back-loop context in which it is placed. To prove this feed- back-compositionality result, we exhibit quadratic-polyno- mial, exponentially decaying bisimulation functions between the IMW and HH-type sodium channels, and also for the IMW-based context in which these sodium-channel models are placed. These functions allow us to quantify the overall error introduced by the sodium-channel abstraction and sub- sequent substitution in the IMW model. To automate the computation of the bisimulation functions, we employ the SOSTOOLS optimization toolbox. Our experimental results validate our analytical ndings. To the best of our knowl- edge, this is the rst application of -bisimilar, feedback- assisting, compositional reasoning in biological systems.

Joint work with A. Islam, A. Murthy, A. Girard and S.A. Smolka

Anvesh Komuravelli - "The SPACER framework -- Automatic Abstractions from Proofs and Counterexamples" PPT

Symbolic model checking for safety properties of programs has taken a new leap with the recent advances in SMT solving. On the one hand, SMT solvers are used to check for the absence of counterexamples of increasing lengths. On the other hand, the model checking algorithms attempt to generalize the bounded proofs of absence of a counterexample, to an inductive proof. Obtaining convergence in practice, however, largely depends on the algorithm's ability to effectively generalize the bounded proofs. Our approach to this problem is to automatically infer and refine good abstractions of the program, which help produce bounded proofs which are easier to generalize. I will discuss our work on inferring quantifier-free loop invariants and some preliminary results on universally quantified invariants.

Soonho Kong - "The dReal/dReach Solver." PDF / WWW / Tools

In this talk, I will introduce our open-source tools dReal and dReach:

1) dReal is an SMT solver for nonlinear formulas over the reals. The tool can handle various nonlinear real functions such as polynomials, trigonometric functions, exponential functions, etc. dReal implements the framework of delta-complete decision procedures: It returns either unsat or delta-sat on input formulas, where delta is a numerical error bound specified by the user. dReal also produces certificates of correctness for both delta-sat (a solution) and unsat answers (a proof of unsatisfiability).

2) dReach is a tool for safety verification of hybrid systems. The tool is able to handle general hybrid systems with nonlinear differential equations and complex discrete mode-changes. It performs bounded delta-complete reachability analysis and uses dReal as a computation engine.

You can find more information on the tools at http://dreal.cs.cmu.edu

Bing Liu - "Parameter identification using delta-decisions for hybrid systems in biology" PDF

Biological systems can possess multiple operational modes with specific nonlinear dynamics in each mode. Hybrid automata and its variants are often used to model and analyze the dynamics of such systems. Highly nonlinear hybrid models are difficult to analysis and usually have many parameters. An important problem is to identify parameter values using which the model can reach certain states of interests. We present a parameter identification framework using delta-complete decision procedures, which can solve SMT problems over the reals with a wide range of nonlinear functions, including ordinary differential equations. We have demonstrated our method on two highly nonlinear hybrid systems: the prostate cancer progression model and the cardiac cellular action potential model. The results show that the parameter identification framework is convenient and efficient for performing model selection, personalized therapy optimization as well as disease-related parameter ranges identification.

Sarah Loos - "Teaching and Proving CPS" PDF

KeYmaera is a verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies. It is an automated and interactive theorem prover for a natural specification and verification logic for hybrid systems. This year we celebrate the sixth anniversary of KeYmaera's public release and in that time we have dramatically upped its proving power and improved its usability. KeYmaera users have had success proving safety properties for many Cyber-Physical Systems, including recent case studies on surgical robotic arms, aircraft collision avoidance maneuvers, and a variety of automotive applications. But, up until this semester, KeYmaera users have been experts and researchers in CPS and/or logic fields. This semester we introduced a new undergraduate course, titled the Foundations of Cyber-Physical Systems (FCPS), at CMU in which undergraduate students quickly advance from learning the basic concepts underlying all hybrid programs to being able to prove safety properties about complex CPS using KeYmaera. In this talk we will combine a tutorial for the KeYmaera tool based on the course design for FCPS with a discussion of pedagogical best-practices for CPS foundations and verification.

Natasa Miskov-Zivanov - "Formal modeling and analysis of timing in biological networks: application to cellular decisions in the immune system" PDF

We use computational modeling and formal analysis techniques to study temporal behavior of a discrete logical model of naïve T cell differentiation, which produces either a T helper cell that coordinates immune responses or a T regulatory cell that suppresses immunity. Understanding how to control the outcome of this process could be critical to the development of new therapies for diseases as diverse as autoimmune disorders and cancer.

The model in [1] represents a generalized form of Boolean network model that allows for modeling elements of the network as discrete variables and their interactions as logic functions. The model couples exogenous signaling inputs to T cell phenotype decisions by including ligands outside of the cell, receptors, signaling molecules inside the cell, transcription factors, and several genes of interest.

We analyzed the model using simulations and formal analysis. The initial set of simulations provided important insights into individual element and overall system behavior. To test hypotheses derived from simulation results, we used statistical model checking and performed queries of a large number of system properties specified in temporal logic. Several key findings resulted from this study. First, we determined probabilities of critical signaling events, as well as temporal behavior of model elements resulting in mixed population of cells and in specific phenotypes. In addition, we found that the system is robust to parameter variations modeled as event delay changes, while it is sensitive to network perturbations. Next, our studies resulted in several predictions about changes in cell population ratios that were later experimentally confirmed. Finally, we identified a number of directions for future experiments and system studies. The results that we obtained in this work and future experimental directions that we outlined can potentially lead to new therapies for a wide range of diseases where immune system function is involved.

Stefan Mitsch - "Provably Safe Obstacle Avoidance of Autonomous Robotic Ground Vehicles" PDF

Nowadays, robots interact more frequently with a dynamic environment outside limited manufacturing sites and in close proximity with humans. Thus, safety of motion and obstacle avoidance are vital safety features of such robots. This talk presents two safety properties and correctness proofs of avoiding both stationary and moving obstacles: (i) passive safety, which ensures that no collisions can happen while the robot moves, and (ii) the stronger passive friendly safety in which the robot further maintains sufficient maneuvering distance for obstacles to avoid collision as well. We use hybrid system models and theorem proving techniques that describe and formally verify the robot’s discrete control decisions along with its continuous, physical motion. Moreover, we formally prove that safety can still be guaranteed despite location and actuator uncertainty.

Ruzica Piskac - "Type Inhabitation Problem for Code Completion and Repair" PDF

Developing modern software typically involves composing functionality from existing libraries. This task is difficult because libraries may expose many methods to the developer. In this talk I will describe a project called InSynth. InSynth synthesizes and suggests valid expressions of a given type at a given program point, to help developers overcome the problems described in the above scenarios. As the basis of InSynth, we use type inhabitation for lambda calculus terms in long normal form. For ranking solutions we introduce a system of weights derived from a corpus of code. I will conclude with an idea how to extend this approach so that it also automatically repairs ill-typed code expressions. This talk is based on joint work with T. Gvero, V. Kuncak and I. Kuraj

Andre Platzer - "Logic of Hybrid Games." PDF

Hybrid systems model cyber-physical systems as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. They arise frequently in many application domains, including aviation, automotive, railway, and robotics. This talk studies hybrid games, i.e. games on hybrid systems combining discrete and continuous dynamics. Unlike hybrid systems, hybrid games allow choices in the system dynamics to be resolved adversarially by different players with different objectives.

This talk describes how logic and formal verification can be lifted to hybrid games. The talk describes a logic for hybrid systems called differential game logic dGL. The logic dGL can be used to study the existence of winning strategies for hybrid games, i.e. ways of resolving the player's choices in some way so that he wins by achieving his objective for all choices of the opponent. Hybrid games are determined, i.e. one player has a winning strategy from each state, yet their winning regions may require transfinite closure ordinals. The logic dGL, nevertheless, has a sound and complete axiomatization relative to any expressive logic. Separating axioms are identified that distinguish hybrid games from hybrid systems. Finally, dGL is proved to be strictly more expressive than the corresponding logic of hybrid systems.

Andreas Podelski - "Proofs that count"

Counting arguments are among the most basic proof methods in mathematics. Within the field of formal verification, they are useful for reasoning about programs with infinite control, such as programs with an unbounded number of threads, or (concurrent) programs with recursive procedures. While counting arguments are common in informal, hand-written proofs of such programs, there are no fully automated techniques to construct counting arguments. The key questions involved in automating counting arguments are: how to decide what should be counted?, and how to decide when a counting argument is valid? We present a technique for automatically constructing and checking counting arguments, which includes novel solutions to these questions.

Joint work with Azadeh Farzan and Zachary Kincaid, University of Toronto

Christoph Scholl - "Verification of linear hybrid systems: Symbolic representations using simple interpolants." PDF

We consider symbolic methods for the verification of linear hybrid automata with large discrete state spaces (where an explicit representation of discrete states is difficult). In particular, we focus on Craig interpolation to simplify and over-approximate representations of large state sets. We compute *simple* interpolants for the theory of linear arithmetic with rational coefficients by successfully minimizing the number of linear constraints in the final interpolant. To this end we make use of several methods including proof transformations, linear programming, and SMT solving. Experimental results show considerable improvements compared to standard methods from the literature.

Christoph Weidenbach - "Beyond SAT and SMT: Automated Reasoning Building Blocks" PDF

SAT and SMT solvers have meanwhile found wide acceptance in research and industry. This is in particular due to a boost in reasoning performance and robustness, due to new calculi and algorithms. In this talk I will identify the relevant building blocks and I will give a forecast on what we can expect in future.

Thomas Wies - "Automated Debugging with Error Invariants" PDF

Debugging is one of the most time consuming aspects of software development. Any automation that reduces the manual effort involved in debugging can have a significant impact on software productivity. An integral part of all debugging activities is the task of fault localization: once undesired behavior is spotted, the actual defect has to be identified before a fix can be developed. I will present a novel technique to automate this task. Our technique is based on the notion of error invariants, which relates fault localization to program verification. I will show how error invariants can be used for slicing error traces, obtaining concise error explanations, and localizing code inconsistencies. The presented algorithms are automated by using interpolating theorem provers to compute suitable error invariants from a faulty program fragment.