HYCON-EECI, Spring 2012

	Specification, Design, and Verification
	of Distributed Embedded Systems
	Richard M. Murray, Ufuk Topcu, and Nok Wongpiromsarn
	14-18 May 2012, L'Aquila (Italy)

Course Description

Increases in fast and inexpensive computing and communications have enabled a new generation of information-rich control systems that rely on multi-threaded networked execution, distributed optimization, sensor fusion and protocol stacks in increasingly sophisticated ways. This course will provide working knowledge of a collection of methods and tools for specifying, designing and verifying networked control systems. We combine methods from computer science (temporal logic, model checking, synthesis of control protocols) with those from dynamical systems and control (Lyapunov functions, trajectory generation, receding horizon control) to analyze and design partially asynchronous control protocols for continuous systems. In addition to introducing the mathematical techniques required to formulate problems and prove properties, we also describe a software toolbox (TuLiP) that is designed for analyzing and synthesizing hybrid control systems using linear temporal logic and robust performance specifications.

Course information

• Instructors: Richard M. Murray (Caltech, CDS) and Ufuk Topcu (Caltech, CDS), and Nok Wongpiromsarn (MIT-Singapore)
• Date and location: 14-18 May 2012, L'Aquila (Italy)
• Sponsor: HYCON-EECI Graduate School on Control

Lecture Schedule

The schedule below lists the lectures that will be given as part of the course. Each lecture will last approximately 90 minutes. The individual lecture pages give an overview of the lecture and links to additional information.

Lec	Date/time	Title	Topics
L1 RM Mon, 9:00	Introduction: Protocol-Based Control Systems	[[EECI 2012: Introduction to networked control systems (NCS) Overview of control "protocols" Examples: Alice, RoboFlag	Introduction to networked control systems (NCS) Overview of control "protocols" Examples: Alice, RoboFlag ]]	{{{5}}}
L2 NW Mon, 11:00	Automata Theory	[[EECI 2012: Finite transition systems Paths, traces and composition of finite transition systems Linear time properties; safety and liveness Examples: traffic light	Finite transition systems Paths, traces and composition of finite transition systems Linear time properties; safety and liveness Examples: traffic light ]]	{{{5}}}
L3 UT Mon, 14:00	Temporal Logic	[[EECI 2012: Linear temporal logic Omega regular properties Buchi automata, representation of LTL using NBA Examples: traffic light, (RoboFlag), autonomous driving	Linear temporal logic Omega regular properties Buchi automata, representation of LTL using NBA Examples: traffic light, (RoboFlag), autonomous driving ]]	{{{5}}}
L4 UT Mon, 16:00	Model Checking and Logic Synthesis	[[EECI 2012: Basic concepts in model checking Use of model checking for logic synthesis Examples: traffic light, farmer puzzle	Basic concepts in model checking Use of model checking for logic synthesis Examples: traffic light, farmer puzzle ]]	{{{5}}}
C1 RM Tue, 14:00 16:00	Computer Session: Spin	[[EECI 2012: Introduction to Promela and Spin (statements, processes, messages) Verification examples: traffic light, distributed traffic light, gcdrive Synthesis examples: traffic light, farmer puzzle, robot navigation	Introduction to Promela and Spin (statements, processes, messages) Verification examples: traffic light, distributed traffic light, gcdrive Synthesis examples: traffic light, farmer puzzle, robot navigation ]]	{{{5}}}
L5 RM Wed, 9:00	Verification of Control Protocols	[[EECI 2012: Brief introduction to abstraction hierarchies for control systems Approaches: deductive approaches, algorithmic approaches (Guarded command languages and CCL) Lyapunov-based proof techniques Deductive verification and barrier certificates Examples: multi-agent systems, RoboFlag	Brief introduction to abstraction hierarchies for control systems Approaches: deductive approaches, algorithmic approaches (Guarded command languages and CCL) Lyapunov-based proof techniques Deductive verification and barrier certificates Examples: multi-agent systems, RoboFlag ]]	{{{5}}}
L6 UT Wed, 11:00	Algorithmic	[[EECI 2012: Abstraction hierarchies for control systems Finite state abstractions (discretization) and model checking Discretization of continuous state systems Approximate bi-simulation (if time) Examples: gear changing (?), ???	Abstraction hierarchies for control systems Finite state abstractions (discretization) and model checking Discretization of continuous state systems Approximate bi-simulation (if time) Examples: gear changing (?), ??? ]]	{{{5}}}
L7 NW Wed, 14:00	Synthesis of Reactive Control Protocols	[[EECI 2012: Open system and reactive system synthesis Satisfiability, realizability Game structures, reachability/safety games Mu-calculus (if time) and GR(1) games Examples: runner-blocker	Open system and reactive system synthesis Satisfiability, realizability Game structures, reachability/safety games Mu-calculus (if time) and GR(1) games Examples: runner-blocker ]]	{{{5}}}
C2 NW Thu, 9:00   Thu, 11:00	Computer Session: TuLiP	[[EECI 2012: Introduction to TuLiP Synthesis of protocols for discrete systems Discretization of continuous systems (and protocol synthesis) Examples: reactive motion planning	Introduction to TuLiP Synthesis of protocols for discrete systems Discretization of continuous systems (and protocol synthesis) Examples: reactive motion planning ]]	{{{5}}}
L9 Fri, 9:00 UT	Receding Horizon Temporal Logic Planning	[[EECI 2012: Receding horizon control Distributed control Examples: reactive motion planning, electric power systems (distributed)	Receding horizon control Distributed control Examples: reactive motion planning, electric power systems (distributed) ]]	{{{5}}}
L10 RM Fri, 11:00	Extensions, Applications, Open Questions	[[EECI 2012: Review of control trends and course contents Discussion of open problem areas and preliminary results Optimization-based techniques Probabilistic techniques Others: Robustness, switching systems, timed systems Examples: robot motion planning, electric power systems (timed)	Review of control trends and course contents Discussion of open problem areas and preliminary results Optimization-based techniques Probabilistic techniques Others: Robustness, switching systems, timed systems Examples: robot motion planning, electric power systems (timed) ]]	{{{5}}}

Software Installation

We will make use of two programs during the lab sessions:

• Spin - model checker for formal verification of distributed systems
• TuLiP - python-based toolbox for temporal logic planning and controller synthesis

During the course, we will access these programs on a remote machine using ssh. For some parts of the course it will be useful to have a local installation of MATLAB that can be used for visualizing some simulation results.

If you would like to install the software on your own, here are some basic directions for installing the two packages:

• Spin: if you are using Windows, you can download a binary installation. For Mac's, you need to compile from source. For this you will need a C compiler, such as the one that is part of the Xcode developer toolbox
• TuLiP: you will need a python installation (2.6 or greater) with SciPy (0.9 or greater) installed. You might consider using the Enthought Python distribution. Once you have scipy installed, you will need to install several other python packages, including cvxopt and yices. A list of required package is available on the TuLiP project page.