Comparing relations

During the past week Jan has continued to work on the validated hybrid IVP solver. One of the components of event detection require the solver to determine when events happen arbitrarily close to an endpoint of the time segment over which event detection is performed. Detection is done by using relations that are known to be true and that comprise the same expressions as the event guard. This means that the zero crossing detection described last week that implements relations as plain Scala functions could not be re-used. Instead, one defines a language of expressions and relations for expressing event guards and invariants, enabling syntactic comparison. The current work focuses on employing the obtained event detection to compute the set of possible events that can occur for a system in a given time segment.  

Intro to Acumen

Anita studied the Core Acumen draft tutorial and started modeling simple electronic circuits both with Acumen and Simulink.

The Uppsala Experience

Jan also attended the UPMARC Multicore Computing Summer School 2012 at Uppsala and thoroughly enjoyed the high-quality seminars that were given. In particular he found the work of Robert Bocchino on Deterministic Parallel Java and the work of Tobias Wrigstad on Structured Aliasing exciting as they present offer concrete ways to reason about sharing in object oriented languages, making it possible to safely code without the risk of introducing data races.    

Multicore and more

During the past week Adam attended the UPMARC Multicore Computing Summer School 2012. A wide range of topics were covered, including verified microkernels, a structured approach to aliasing in OO languages and an effect-tracking approach to deterministic execution of object-oriented code. A particular highlight was the lecture series by Martin Vechev. There, a method for "Machine-Assisted Concurrent Programming" was presented where conservative overapproxmations (based on abstract interpretation) are used not only to prove correctness of programs but also to introduce changes in the programs which remedy defects detected during verification. For example, this can be used to automatically introduce atomic sections and fences in concurrent code. 

Muzeyen deposits masters thesis

Muzeyen has completed and deposited his masters thesis at Halmstad University.  The title of his thesis is "Modeling Basic Physical Links in Acumen."  The thesis compares Acumen, MATLAB, and Simulink using a benchmark of models representing a physical link.  The link consists of an electrical channel made of a resistive and a capacitive component, and several different modulation/demodulation schemes.  The thesis, defense presentation, and all related Acumen models can be found in online archive available from the group website.  Muzeyen and Anita will be working on writing up the results as a conference submission.

Zero crossing

During the past week Jan has implemented event detection using first-order interval polynomial arithmetic. For the purpose of simulating hybrid ODEs it is necessary to determine when an event must have happened and when an event may have happened in a given time interval. Below follow two plots showing zero-crossing detection for solutions to the ODE 

x'' = -10, x'(0) = 0, x(0) = 5 for times t in [0,2] 

where the solution is computed with a uniform step size of 0.2. In the following plot solving is halted when there is certainty that the solution must have crossed zero somewhere in the last time step.  

and in the following plot solving is halted when there is a possibility that the solution may have crossed zero somewhere in the last time step.  

Symbolic differentiation with subexpression sharing

This week Yingfu and Adam started working on an implementation of symbolic differentiation for expressions in Scala. A differential operator implementation is ready for a small expression type including a few operators. An interesting part of the implementation is the subexpression sharing mechanism. Here, an "expression context" is used to maintain a collection of references to intermediate expressions (corresponding to a list of let bindings). Constructors of the expression types are not called directly in the program. Instead, factory methods are used for instantiation, which first look in the expression context to see if an existing instance can be referenced. A simple way to implement the expression context is to use a Scala Map object. Here, it is possible to leverage the default implementations of the hashCode method which come with Scala case classes, making it possible to use the expressions themselves as keys in the map.

As a concrete example, consider differentiating the expression x^2 + x^2 with respect to x. The result of applying our symbolic differentiation operator is the following (in pseudocode):

let

  x_4 = Plus(x_0,x_0)

  x_1 = Times(x_0,x_0)

  x_5 = Plus(x_4,x_4)

  x_2 = Plus(x_1,x_1)

  x_3 = Literal(1.0)

  x_0 = Variable("x")

in

  x_5

Who can handle Zeno

During the past week's CyPhy workshop Jan learned that there are no general purpose tools for simulation of hybrid systems that correctly handle Zeno points. Zeno points of a hybrid system are those times that have a bounded neighborhood in which the system makes an infinite number of transitions. The state of the art is to employ symbolic heuristics to detect Zeno points, but even mature tools such as OpenModelica can generate erroneous simulations at and following Zeno points. There is thus a need for hybrid simulators that can detect, or at least indicate the presence of Zeno points.

Amber model and Modelica tutorial

The two most interesting point Mingkun picked up from CyPhy workshop are the mathematical model of Amber robot and the way how tutorials of Modelica are presented. Amber model illustrates how simple the model could become once the most significant parts of the problem are identified. However, the performance of simulation is limited by the poor symbolic computation ability, which demands quick improving. Despite of the issue of platform-dependent, the process of following tutorials of Modelica is very enjoying. Users can get immediate feedback from this.

A formidable optimization challenge

This week Adam participated in CyPhy 2012, a workshop on Cyber-Physical Systems. He found it interesting to see people with such varied backgrounds as programming languages, robotics, communication and bioinformatics come together in a common discussion. A particular eye-opener for Adam was how much room for improvement there can be in simulation models implemented in industrial-strength (but generic) tools such as Mathematica and Matlab. A specific model from robotics presented at the workshop would require a computation that currently takes two hours to be performed in ten milliseconds in order to be considered real-time. This is a formidable optimization challenge, one where current research can be applied to great benefit (see paper Mathematical Equations as Executable Models of Mechanical Systems) and a great example of why computer scientists and domain experts have a lot to gain from talking to each other.