search

heron-solver / heron

🏺 Simulation Solver for Timed Causality Models in TESL
MIT License
5 stars 1 forks source link
event-driven logical-time modelling polychronous real-time simulation solver synchronization

readme

Heron Build Status GitHub Version Try with Docker

Running on Radiotherapy.tesl

Heron [1, 2, 5] is a solver for the Tagged Events Specification Language (TESL) [3], a declarative language for specifying synchronization of discrete events for simulation. This prototype provides:

  1. Definition of TESL specifications for causality and time scale between events.
  2. Simulation by sound and complete generation of execution traces.
  3. Scenario testing.

Getting started

Try me with Docker

The easiest way to start with Heron is to get Docker and then simply type

$ docker run -it nguyenvanhai/heron
# ./heron --use examples/basic/FirstExample.tesl

Binary distribution

You can also fetch the latest binary release for your operating system (Linux and macOS).

Examples

[4] SNE, Jun 2020 [5] TIME 2020
Cessna 172 Takeoff Radiotherapy machine
Airbus A320 Autobrake Proportional–integral–derivative Controller
Airbus A320 Accelerate-Stop Timed Automaton

For more information, please refer to the Heron Reference Manual.

Research

  1. On the Semantics of Polychronous Polytimed Specifications, Formal Modeling and Analysis of Timed Systems (FORMATS), 18th International Conference, Sept 1-3, 2020.
  2. A Symbolic Operational Semantics for TESL with an Application to Heterogeneous System Testing, Formal Modeling and Analysis of Timed Systems (FORMATS), 14th International Conference, Sept 5-7, 2017.
  3. TESL: a Language for Reconciling Heterogeneous Execution Traces, Formal Methods and Models for Codesign (MEMOCODE), 2014 Twelfth ACM/IEEE International Conference, Oct, 2014, 114-123.
  4. Timed Discrete-Event Simulation of Aviation Scenarios, Simulation Notes Europe, Volume 30(2), June 2020.
  5. TESL: a Model with Metric Time for Modeling and Simulation, Temporal Representation and Reasoning (TIME), 27th International Symposium, Sept 23-25, 2020.

People

The project is named after Heron of Alexandria, the first-century Greek mathematician and engineer. It uses MPL and MLton as its Standard ML compiler. Contributions by Hai Nguyen Van, Thibaut Balabonski, Frédéric Boulanger, Chantal Keller, Benoît Valiron, Burkhart Wolff.

License

Heron is released under the MIT License.

THE PROVIDER MAKES NO REPRESENTATIONS ABOUT THE SUITABILITY, USE, OR PERFORMANCE OF THIS SOFTWARE OR ABOUT ANY CONTENT OR INFORMATION MADE ACCESSIBLE BY THE SOFTWARE, FOR ANY PURPOSE. THE SOFTWARE IS PROVIDED "AS IS," WITHOUT EXPRESS OR IMPLIED WARRANTIES INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, OR NONINFRINGEMENT WITH RESPECT TO THE SOFTWARE. THE PROVIDER IS NOT OBLIGATED TO SUPPORT OR ISSUE UPDATES TO THE SOFTWARE.