Comparing Acumen to a framework for hybrid system verification

During the past week Adam has extended a report comparing Acumen to related work with the paper "Design principles for an extendable verification tool for hybrid systems" by Frehse and Ray. The paper describes a framework which bears some interesting similarities to Acumen. The framework provides APIs and components on which several semantics for a hybrid system model can coexist and share functionality. The emphasis in this framework is on verification, and example semantics (instances of the abstract framework APIs) based on Linear Hybrid Automata and Support Functions are given in the paper. Further, Adam has continued working on the virtual experimentation paper.

Simpler event handling

Last week Jan worked on improving the support for nonlinear invariants in Acumen's enclosure semantics and on alternative simulation time subdivision strategies. Michal and Jan also managed to simplify the event handling algorithm, by removing enclosures entirely from the event tree, so that it can be built up using vectors of intervals. The main benefit of this change, besides the simplification of the specification and implementation of event handling, is that the use of invariants to improve enclosures can now be easily described in terms of intersection of interval boxes. In the coming week Jan will make a formal analysis of the algorithm worked out for a simple example, and on a simplification of the solver algorithm specification.

Two papers and a library related to Acumen's enclosure semantics

During the past week Adam has been comparing the enclosure semantics of Acumen to three sets of algorithms that address the problem of reliability in simulations of hybrid systems. The first one, described in An asynchronous integration and event detection algorithm for simulating multi-agent hybrid systems by Esposito et. al. is an algorithm for simulating hierarchical, multi-rate, hybrid systems in which event detection is guaranteed and which makes it possible to simulate using a lower average integration rate. The second one, described in Robustness of Model-based Simulations by Fainekos et. al. is a method for statically analysing a concrete Simulink simulation in order to detect whether uncertainties in the inputs or parameters of the model, or computational errors, could have produced a result that differs from that of the given simulation. The analysis compares the sequence of Simulink blocks traversed by the simulation and warns the user if a different sequence is possible given the uncertainties present in the model, or due to floating point computation errors. The third set of algorithms is a MATLAB toolbox for validated numerical computation called INTLAB. It includes several data types and algorithms which are useful when building validated ODE IVP solvers like that of Acumen's enclosure semantics, including interval- and interval polynomial arithmetic, validated standard function approximations, integration of such functions as well as automatic differentiation. During the coming week Adam will focus on writing a survey of tools for virtual experimentation.

Computing mode invariant sets

Last week Jan worked on the enclosure interpreter, mainly focusing on additions that support more complex benchmarks. A modified version of the bouncing ball model, which tracks the energy of the ball as well as its position and velocity, has been the guiding example. The most demanding of the required additions is the computation of the support set of mode invariant predicates which comprise nontrivial numeric expressions. It is this set that allows the interpreter to use the mode invariant to reduce the over-approximation of the computed enclosures. Jan's idea was to enclosure-evaluate the expressions in the invariant and then use a simple interval constraint solving technique to compute a conservative approximation of the support. While this approach works well for linear expressions and for nonlinear expressions in one variable, mixed-variable nonlinear expressions lead to excessive over-approximation of the support. Jan suspects that this over-approximation may be one of the reasons why the benefits of adding the energy to the bouncing ball model could not be observed. Jan also spent some time experimenting with an alternative strategy for subdivision of the simulation time. In the coming week Jan will continue to work on the invariant support computation algorithm.

Studying at Rice

Yingfu has been studying at Rice for two months and just finished two mid-term exams last week.  The course "Principles of programming languages" taught by Cartwright is very interesting which not only focuses on building blocks, semantics and type systems of programming language but also introduces some fundamental concepts including alonzo church's lambda calculus back to 1930s.  And the projects are using Scala to write a small functional language called "Jam".  The course "System dynamics" taught by Marcia teaches yingfu some mechanical background starting with the classic mass-spring-damper systems.  The last course is  Algorithmic Robotics taught by Lydia, which introduces many algorithms for doing motion planning.

 

Starting a survey of tools for hybrid system state space exploration

During the past week Adam completed a draft digest of Carloni et al. In the coming week he will start writing a survey of hybrid system verification tools focused on their support for state space exploration. Such tools allow the user to visualise a conservative approximation of the state of a hybrid system over time.

Plotting enclosures

Last week Kevin and Jan and Adam continued to improve the Acumen IDE support for enclosure plotting. Kevin enabled the IDE to display the so-far computed enclosures as they are generated. The progress bar also shows the percentage of the time domain for which enclosures have been computed. Adam modified the way enclosures are displayed so that a single region is shown for each time segment and that the border of the region is clearly demarcated. Jan has been adding fearures, such as extending the syntax with intervals and implementing a simple constraint solver, that will make it possible to simulate more complex benchmarks using the enclosure semantics.

In the coming week Kevin will be improving and simplifying the GUI and interpreter interface code. Jan will focus on further extending and improving the enclosure interpreter as well as finalizing the support for the more complex benchmarks.

First half of digest of hybrid systems survey

During the past week Adam worked on a digest of the Languages and Tools for Hybrid System Design survey. He covered the simulation tools and languages and during the coming weeks aims to cover verification tools as well as the comparative study part of the survey.

Moving integration forward

Last week Kevin and Jan continued the integration work. They provided support for plotting of the so-far computed enclosures when halting computation using the stop button. Kevin implemented a trace view for enclosure values and prepared a first version of the IDE with 3D visualization and enclosure semantics support. Jan also added support for setting of solver parameters from within an acumen program.

In the coming week Kevin will work on adding missing IDE features for the enclosure semantics, such as displaying enclosures as they are computed. Kevin will also look into improving the overall quality of the IDE user experience and the recently added features. Jan will add more benchmarks for enclosure simulation and work on the necessary functionality in the interpreter to support these benchmarks. One such addition will be the lifting of restrictions on the expressions allowed in event guards.