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.

Progress on the enclosure semantics integration front

Last week Kevin and Jan continued the ongoing integration work. An initial version of support for plotting of enclosures was implemented. Kevin also implemented support for starting and halting the enclosure solver from within the Acumen IDE, as well as displaying the enclosure solver's progress reports in the IDE console. Jan extended the syntax supported by the enclosure semantics to include higher derivatives. Adam also helped in discussions about how to change the architecture of the Acumen environment to provide common infrastructure for the different semantics.  

In the coming week Kevin and Jan will focus the integration work on completing a minimal set of features needed to provide a demonstration version of the Acumen IDE using the enclosure semantics. In particular, they will implement a trace view for enclosure values at time-segment endpoints, plotting of the so-far computed enclosures when halting mid-computation and support for setting of solver parameters. In the longer term the main aim is to relax the restrictions on control structures currently supported by the enclosure semantics. 

Writing about tools for hybrid systems design

During the past week Adam has been working on a summary of the survey Languages and Tools for Hybrid Systems Design and has worked on developing a problem formulation for a report about hybrid systems tools and languages. In the coming week Adam aims to finish writing the summary and to refine the problem formulations.

Continuing the enclosure semantics integration work

Previously, Adam and Jan have been working on the integration of the enclosure-based hybrid solver with Acumen. The integration work has centered around the extraction of the hybrid automaton representation of Acumen models that is required by the solver. They also made some necessary additions to the Acumen syntax, the GUI and command line front-ends. 

In the coming week Adam and Jan will work on the design and implementation of the enclosure simulation data representation that will interact with the plotter through the abstract interface developed by Kevin and Jan. Adam and Jan will also develop initial solutions for the setting of simulation parameters through Simulator object.