Module2 - mtrl - Formal Methods

Motivation

Formal methods are, generally speaking, rigorous techniques for specification, analysis and verification of systems. Autonomous systems are often safety-critical, or mission-critical, meaning that their malfunctioning may cause severe harm to humans or financial loss. Think of airplanes, autonomous cars, industrial robots operating in proximity to people. In all of these systems, faulty design may have fatal consequences.

Formal methods ultimately aim to ensure that systems work as they are expected in a principled way. Three main formal methods approaches are formal verification, falsification, and formal synthesis. Formal verification answers: given a system model and rigorously specified requirements, prove that the system model meets the requirements, or give a counter-example when it does not. Falsification aims to systematically reveal errors. In formal synthesis, a system model, a controller for a given system model, or even a computer program in a programming language like C or C++, are algorithmically synthesized from a given set of rigorously specified requirements.

It should be noted that formal methods are not a substitute for testing and simulations. They complement these techniques and they do come with some limitations: The vast majority of formal methods techniques require a system model and rigorous specification of requirements. This means that all guarantees they can offer hold for the model, and one has to be careful when making claims about the system guarantees. The application of formal methods in real life is challenging in particular because:

Complexity of the autonomous system and its environment creates gap between reality and system model; and
Complexity of models and requirements make verification, falsification, or synthesis questions undecidable, or computationally demanding, or in practice sound, but not complete.

As of today, formal methods are useful especially to:

Systematically reveal errors and bad design choices
Improve understanding about the systems and increase trust in that they work as expected
Achieve guarantees under assumption
Aid system design

We will focus here on temporal logics as a specification language and model-checking as a core verification/falsification/synthesis technique. However, traditional specifications and formal methods coming from the theoretical computer science community also include mu-calculus, theorem proving, SMT solving, deductive verification, and others. Some techniques coming from the hybrid systems/control systems community, such as reachability analysis can be viewed as formal methods, too.

Learning Outcomes

You should be able to describe what formal methods are, the main approaches, what they are used for and give examples of challenges. You should be able to give concrete examples. You should be able to describe what model-checking is and roughly how it works. You should be familiar with LTL as a way to rigorously specify a desired system behaviour, transition systems as a way to describe a system and LTL, transition systems, and Büchi automaton. You should be able to desribe, in general terms, what formal synthesis is.

Model-checking

The term refers to the act of checking (exhaustively and automatically) whether a property (specified as a formula) holds or not for a given model.

Model Checking Intro Links to an external site. (3:14min)
A very good introduction to model checking can be found in the first chapter of Clarke, Edmund M., et al. Handbook of model checking. Springer, 2018. Links to an external site.

LTL automata-based model-checking

A good start to LTL automata-based model-checking is to get familiar with three key terms: LTL, transition systems, and Büchi automaton. Links to an external site. A brief introduction:

LTL Teaching slides of professor Alessandro Artale at the Free University of Bozen-Bolzano
Example on state-transition diagram (also called transition system or Kripke structure) Links to an external site.

The figure below illustrates the principle for a discrete labelled transition system and a linear temporal logic formula.

LTL automata-based model checking overview

The question is "Do all executions satisfy the temporal logic formula?". Model-checking turns this into a question that is easier to answer algorithmically: "Does there exist an execution that violates the formula?" In other words, does there exist an execution that satisfies the negation of the formula?". That is why the first step is formula negation. Next, the formula is translated into a Büchi automaton Links to an external site.. The translation is a quite involved process. There are some off-the-shelf tools out there that you can try out, such as Spot. Links to an external site. Next, a product between the system model and the specification automaton is built. This product represents behaviors that are allowed by the system and satisfy the negation of the formula. The product is also a Büchi automaton. If an accepting path can be found in the product, this serves as a an example where the negation of the formula holds, ie. or a counterexample of the desired property. This counterexample can be useful to understand why the property is not fulfilled within the system model and to consequently fix the system.

For different types of models and specification languages, this process differs slightly, but the overall process remains similar. There exist a multitude of tools for different purposes, a small overview can be found here Links to an external site.. Other common approaches, models and specification languages:

Model checking of timed systems

Timed automata is a frequently used model, which keep track of time and put time restrictions on transitions between states
A frequently used specification language is Metric Interval Temporal Logic, an extension of LTL that is able to reason about intervals of time (something should happen every 5 seconds, a response to every request should come within 10 minutes, etc.)

Notable tools: UPPAAL. Links to an external site.

Probabilistic model checking

In probabilistic model checking a typical model is Markov chain or Markov Decision Process
In terms of specification, we are interested in a seeing whether a certain LTL formula holds with desired probability. A frequently used language is also a branching logic PCTL.

Notable tools: PRISM Links to an external site., STORM Links to an external site.

[Additional material] Slides from a Probabilistic Model Checker course (19 lectures, many hours of fun!) Links to an external site.

Formal synthesis

Formal synthesis is dual to formal verification. Instead of searching to prove or falsify a property on the model, formal synthesis tries to generate a model or a strategy from a given specification. Usually, this involves combining a model of the environment with a specification automaton, similar to Figure 1. A very nice paper overviewing formal synthesis for robotics is
Hadas Kress-Gazit, Morteza Lahijanian, and Vasumathi Raman, Synthesis for Robots: Guarantees and Feedback for Robot Behavior, Annual Reviews 2017. Links to an external site.

With spare time and interest you might also want to have a look at the paper "Synthesis of Control Protocols for Autonomous Download Synthesis of Control Protocols for Autonomous

Systems Download Systems" that surveys LTL, model verification and describes the tool TULIP, with some application to autonomous driving.

Students with a background on control should also have time to do the following (not needed to do the quiz on Verification)

install PRISM, a tool for probabilistic model checking, described below
do PRISM Example 1 (6-sided dice) described below

PRISM model checker

There are many model checkers. Among these, we have selected PRISM, a probabilistic model checker. PRISM allows modelling and analysis of systems that exhibit probabilistic behavior. It has been used to analyze systems from many different application domains Links to an external site., including communication and multimedia protocols, randomized distributed algorithms, security protocols, biological systems and many others.

Introduction to PRISM Links to an external site. (3:40min)

Additional materialModel Checking and Strategy Synthesis for Stochastic Games: From Theory to Practice Links to an external site. (42:39min)

PRISM Tutorial at the Marktoberdorf summer school, 2011 Links to an external site.

PRISM can be used to analyze several different types of probabilistic models, including discrete-time Markov chains (DTMC), continuous-time Markov chains (CTMC), Markov decision processes (MDP) and probabilistic extensions of the timed automata formalism (PTA). Properties to be verified against these models are expressed in probabilistic extensions of temporal logic.

Installation

Download the latest version of PRISM from the official website Links to an external site. (available for all major OS. But only installation on Ubuntu 16.04 has been verified by us.). When you unpack the downloaded file you will see a file structure that resembles the following. The following instructions assume that BASEDIR is the folder where you have unpacked your PRISM files.

|- bin
|- doc
|- etc
|- examples
|- lib
CHANGELOG.txt
COPYING.txt
install.sh
README.txt

Execute the install script with the following command. The install script only changes the environment variable to locate the PRISM directory.

cd BASEDIR /* directory where you have unpacked the files */
./install.sh

The bin folder contains the binary files for PRISM (prism and xprism). To execute prism move to the folder and execute the command.

cd BASEDIR /* directory where you have unpacked the files */
./bin/xprism

This will open the graphical interface.

Now you can write your first PRISM model. Open the tutorial Links to an external site. page and follow the examples that are shown on the website. In particular, study the following example:

Example 1 Links to an external site.: This uses a simple discrete-time Markov chain (DTMC) example - a randomised algorithm for modelling a 6-sided die with a fair coin. It introduces the basics of the PRISM modelling language and the PRISM tool.

Additional:

Example 2 Links to an external site.: This uses another simple randomised algorithm - Herman's self-stabilisation algorithm, which is also modelled as a DTMC. It introduces some additional features of the PRISM modelling and property languages.
Example 3 Links to an external site.: This introduces a continuous-time Markov chain (CTMC) example and is based on an analysis of dynamic power management systems in PRISM.

Guided larger example

We will now create one additional example. We want to model potential sensor failures in a control system. The control system is composed of n sensors, belonging to the set $S = {s 1, s 2, \dots s n}$ $\mathcal{S} = \lbrace s1, s2, \dots sn \rbrace$ and a controller. The controller is invoked at every time instant k and receives as input the vector $y (k)$ $\mathbf{y}(k)$ that contains the values read by the sensors , $y (k) = [y_{1} (k); y_{2} (k); \dots; y_{n} (k)]$ $\mathbf{y}(k) = [ y_1(k); y_2(k); \dots; y_n(k) ]$ . We assume that all the sensors are equal and that they have a failure probability $p_{f}$ $p_f$ . Moreover, we assume that at a given time instant, only one sensor can fail. We denote with $S_{s}$ $\mathcal{S}_s$ the set of sensors that are successfully producing values, and with $S_{f}$ $\mathcal{S}_f$ the set of sensors that are currently experiencing failures.

If the set of failing sensors is not empty, i.e., if $S_{f} \neq \emptyset$ $\mathcal{S}_f \neq \emptyset$ , at each time instant one sensor can be repaired. We denote with $p_{r}$ $p_r$ the probability that the chosen repair operation is successful. Finally, we assume that the controller can operate if and only if at least a fraction $p_{n}$ $p_n$ of the sensors are successfully producing data.

We want to model this situation with PRISM and take advantage of the probabilistic model checking functionalities to verify given properties on quantities like the percentage of correct invocations of the controller, given some parameter set ${n, p_{f}, p_{r}, p_{n}}$ $\lbrace n, p_f, p_r, p_n\rbrace$ . First we need to select the type of model. For our purposes, an MDP model is enough. We will then model separately the set of sensors and the controller. For these two entities we will use modules. The percentage of correct invocations of the controller is going to be computed in a reward structure. The code skeleton is as follows

mdp

// definition of general parameters
const int NUM_SENSORS = 15;
const double PRO_SENSOR_FAIL = 0.8;
const double PRO_SENSOR_REPAIR = 0.8;
const double PERCENTAGE_NEEDED_FOR_CORRECT_OPERATION = 0.5;

module sensors
endmodule

module controller
endmodule

rewards "percentage_correct"
endrewards

Now we have to fill in the description of the behavior of the two modules and of the reward function. We want to enforce a precedence between the action of the modules. First, we want the sensors module to determine how many sensors are currently working, based on the previous state of the system and on a probabilistic transition determining if one sensor is failing. Second, we want to use this information in the controller module to determine if the operation is carried out successfully or not.

To implement this logic we define a turn variable, that can have values in the interval [0..1] and with initial assigned value zero. The fact that turn is a global variable ensures that all the modules can modify it. We will encode that leaving the module sensors, the turn variable will be set to one, and leaving the module controller it will be set to zero. A global variable cannot be modified in labelled transitions.

// The global variable turn cycles between
//   - 0 (collect data from the sensors)
//   - 1 (invoke the controller execution)
global TURN: [0..1] init 0;

Now we have all we need to define the module sensors. We include a local variable s that contains the number of currently working sensors. This variable can assume values in the interval [0..NUM_SENSORS]. The value current_fail determines if there is a current failure or not. The value current_repair determines if one sensor is being repaired. The module will have three different transitions, executed one after the other. In the entry point, we determine (based on $p_{f}$ $p_f$ ) if there is a failing sensor. When this check is executed, we determine (based on $p_{r}$ $p_r$ ) if there is a repaired sensor. Finally, we update s and pass the turn to the controller.

module sensors

  // s contains the number of working sensors
  s : [0..NUM_SENSORS] init NUM_SENSORS;
  current_fail : [0..1] init 0;
  current_repair : [0..1] init 0;
  fail_check : bool init false; // done fail check?
  repair_check : bool init false; // done repair check?

  // check if a sensor is failing (probabilistic transition)
  // this does not check if all are sensors are in fail
  // state already (it could be easily done)
  // we implement the check using the max operator
  // in the last transition
  // HERE: it is my turn and
  //       I have not done fail and repair checks
  [] (TURN=0 & !fail_check & !repair_check) ->
         PRO_SENSOR_FAIL  : (current_fail' = 1) & (fail_check' = true) +
      (1-PRO_SENSOR_FAIL) : (current_fail' = 0) & (fail_check' = true);

  // check if a sensor is being repaired at this point in time
  // --> if possible to repair some (there is at least one that is in fail state)
  //     probabilistic transition
    // HERE: it is my turn, I have done the fail check, and
  //       I have not done the repair check
  [] (TURN=0 & fail_check & !repair_check & s<NUM_SENSORS) ->
         PRO_SENSOR_REPAIR  : (current_repair' = 1) & (repair_check' = true) +
      (1-PRO_SENSOR_REPAIR) : (current_repair' = 0) & (repair_check' = true);
  // --> if not possible to repair some (none is in fail state)
  [] (TURN=0 & fail_check & !repair_check & s=NUM_SENSORS) ->
         (current_repair' = 0) & (repair_check' = true);

  // update the number of working sensors and then pass the turn to the controller, notice the max operator (a "min" is
  // not needed, because the repair check is based on the
  // number of sensors in fail state)
  [] (TURN=0 & fail_check & repair_check) ->
         (s' = max(0, s - current_fail + current_repair)) & // set working sensors
         (fail_check' = false) & (repair_check' = false) & // reinitialize
         (TURN' = 1); // pass the turn to the controller

endmodule

Finally we can write the controller module. We want to label the transition with the correct operation and the transition with the incorrect operation to facilitate writing reward structures based on which transition is taken. Once we determine if the controller executed correctly, we can pass the turn to the sensors again.

module controller
  correct_invocations: int init 0;
  total_invocations: int init 0;
  decided_if_correct: bool init false;

  [correct] (TURN=1 & !decided_if_correct & s >= PERCENTAGE_NEEDED_FOR_CORRECT_OPERATION * NUM_SENSORS) ->
     (correct_invocations' = correct_invocations + 1) &
     (total_invocations' = total_invocations + 1) &
     (decided_if_correct' = true);

  [incorrect] (TURN=1 & !decided_if_correct & s < PERCENTAGE_NEEDED_FOR_CORRECT_OPERATION * NUM_SENSORS) ->
     (correct_invocations' = correct_invocations) &
     (total_invocations' = total_invocations + 1) &
     (decided_if_correct' = true);

  [] (TURN=1 & decided_if_correct) ->
     (decided_if_correct' = false) &
     (TURN'=0);

endmodule

Finally, we can write the reward structure for the percentage of correct invocations.

rewards "percentage_correct"
  true : correct_invocations/total_invocations;
endrewards

We could also write rewards structures using labelled transitions, like the following two. In this case we are counting the amount of correct invocations based on the transition that is taken, and the amount of total invocations rewarding both the correct and the incorrect transitions.

rewards "total_correct"
  [correct] true : 1;
endrewards

rewards "total_invocations"
  [correct] true : 1;
  [incorrect] true : 1;
endrewards

We can simulate the system now (the simulation determines one path and shows it to the user, it does not take advantage of the full model checking). The simulation that you see in the following pictures is obtained with n=15, $p_{f}$ $p_f$ =0.8, $p_{r}$ $p_r$ =0.7, and $p_{n}$ $p_n$ =0.5. The length of the simulation has been extended compared to the standard one.

We can then define properties to verify. One example is what is the minimum percentage of correct invocations that we can obtain in 100 invocations? We can then simulate or verify the property. If we simulate it, it means that we are running Monte Carlo simulations and determining bounds based on the results of the simulations. If we verify the property, we are using model checking to check exhaustively all the states (don't do it with this property, it will not terminate).

Property specification Download Property specification

Different computation engines can be chosen for verification purposes, see the PRISM manual for details. Depending on the type of model and on the amount of branches that the solver should traverse, some solvers are more efficient than others. Also, not all the solvers support all the types of properties.