Chair: Pieter J. Mosterman
Hybrid System Software
The software classification is based on the primary focus of a package. For example, the Chi design system is listed as a specification package, but a simulation engine is also available.
ESCHER is an independent, non-profit research institute dedicated to the transition of government-sponsored information-technology out of the research environment and into practical use by industrial and government end users.
Mathtools is a technical computing portal for all scientific and engineering needs. The portal is free and contains over 20,000 useful links to technical computing programmers, covering MATLAB, Java, Excel, C/C+, Fortran and others.
DSM Forum exists to spread the knowledge and know-how of Domain-Specific Modeling (DSM). DSM raises the level of abstraction beyond programming by specifying the solution directly using domain concepts. It is an independent body made up of the leading DSM tool and solution providers, along with expert DSM users.
ABACUSS (Advanced Batch And Continuous Unsteady-State Simulator), developed for chemical engineering systems, supports hybrid models, model inheritance, hierarchical model decomposition. It facilitates guaranteed state event location, batch process simulation, solution of high-index differential algebraic equations, dynamic and steady-state optimization, and dynamic sensitivity and uncertainty analyis.
DAEPACK is a software library for general numerical calculations. It is divided into two major libraries: symbolic analysis and transformation and numerical calculation. The symbolic analysis and transformation library consists of components for analyzing general Fortran-90 models and automatically generating the information required when using modern numerical algorithms, e.g., (i) sparsity pattern generation, (ii) discontinuity locking, and (iii) automatic differentiation.
AnyLogic is a professional virtual prototyping environment. It enables you to rapidly build a simulation model of the system under development and its environment, including physical objects and human users. The modeling technology is based on UML-RT, Java, and algebraic-differential equations. AnyLogic offers a range of domain-specific libraries.
BaSiP is developed for simulation of recipe-driven production in complex multi-purpose batch plants.
DOORS zielt auf die Erstellung eines Prototyps für einen verteilten, echtzeitfähigen Simulator, der den Entwurfsprozeß mechatronischer Systeme bis zum Hardware-in-the-Loop-Test unterstützt.
Dymola provides a powerful object oriented modeling and simulation environment for education and the professional engineer.
gPROMS represents the state-of-the-art in process modelling, simulation and optimisation technology.
HYBRSIM is an implementation of a hybrid bond graph modeling and simulation tool. It embodies a set of physical principles that govern discontinuous changes in physical system models.
Model Vision 3.0 is an object-oriented environment for the design of large dynamic systems that features: (i) Supporting B-Charts (UML-compatible statecharts integrated with differential equations) to specify hybrid behavior, (ii) Numerical methods from ODEPACK and Hairer-Norsett-Wanner collection, (iii) Supports matrix and vector data types, (iv) Includes standard device class libraries and enables the user to create his own, (v) Animation libraries and wizards for rapid creation of animated sketches, (vi) Generates complete portable Win32 and Java executable models supporting automation.
OmSim is an environment for modelling and simulation based on Omola. Omola is an object-oriented language for modelling of continuous time and discrete event dynamical systems.
SHIFT is a programming language for describing dynamic networks of hybrid automata. Such systems consist of components which can be created, interconnected and destroyed as the system evolves. Components exhibit hybrid behavior, consisting of continuous-time phases separated by discrete-event transitions.
Smile is a simulation tool for energy systems. A ZimOO (an object-oriented specification language for hybrid systems in which continuous aspects are modeled by differential equations) specification of a simulation model serves as the basis for implementing the model in the simulation language Smile.
20-SIM ("Twente Sim") is a modeling and simulation program that runs under Microsoft Windows and Sun-Unix. With 20-sim you can simulate the behavior of dynamic systems, such as electrical, mechanical and hydraulic systems or any combination of these systems.
HyTech is an automatic tool for the analysis of embedded systems. HyTech computes the condition under which a linear hybrid system satisfies a temporal requirement. Hybrid systems are specified as collections of automata with discrete and continuous components, and temporal requirements are verified by symbolic model checking. If the verification fails, then HyTech generates a diagnostic error trace.
KRONOS is a tool developed with the aim to verify complex real-time systems. Components of real-time systems are modeled by timed automata and the correctness requirements are expressed in the real-time temporal logic TCTL. KRONOS checks whether a timed automaton satisfies a TCTL-formula.
MOBY comprises a graphical editor for (i) PLC-Automata, a formal description technique for real-time systems, (ii) SDL-Specifications, and (iii) Object Z-Specifications. These specifications can be used for model checking (based on timed automata) and (graphical) simulation (based on high level Petri nets).
Spin is a widely distributed software package that supports the formal verification of distributed systems. The software was developed at Bell Labs in the formal methods and verification group.
STeP, the Stanford Temporal Prover, is being developed by the REACT research group to support the verification of reactive, real-time and hybrid systems based on their temporal specification. STeP is not restricted to finite-state systems, but combines model checking with deductive methods to allow the verification such systems as parameterized (N-component) circuit designs, parameterized (N-process) programs, and programs with infinite data domains.
UPPAAL is a tool suite for validation and verification of real-time system modelled as networks of timed automata extended with data variables. The tools have WYSIWYG interfaces and features: graphical editing, graphical symbolic simulation and symbolic verification.
Verdict ist der Name eines Rechnerwerkzeuges zur formalen Verifikation diskreter Steuerungen für kontinuierliche Prozesse, wie sie zum Beispiel in verfahrenstechnischen Anlagen häufig anzutreffen sind. Die formale Verifikation ist ein Verfahren, mit dem ein mathematischer Nachweis darüber erbracht werden kann, daß eine gegebene Steuerung einen bestimmten technischen Prozeß in jeder denkbaren Situation so beeinflußt, daß eine getrennt vorgegebene Anforderungsbeschreibung an das gewünschte Prozeßverhalten eingehalten wird.
visualSTATE is a suite of tools, that supports you all the way through the software development process in an iterative and interactive specification process. You rapidly create a virtual prototype of an an outline of your product that can be evaluated and validated against the specification. visualSTATE automatically generates code for your target system and the Tester tools and techniques include interactive simulation, real-link for in-target testing and complete dynamic formal verification.
The Chi design system is a concurrent programming language based on the (Timed) CSP formalism. The Chi language can be used to express models of industrial systems. A model expressed in Chi is simulated using the Chi simulator.
The Compositional Modeling Language (CML) is a general declarative modeling language for specifying the symbolic and mathematical properties of the structure and behavior of physical systems. It intendeds to facilitate the construction and accumulation of sharable models of core engineering domains.
The Hybrid CC language is a compositional modeling language for physical systems. It started with Concurrent Constraint programming languages, which provide the fine grained concurrency desirable for compositionality. They are very expressive, being built on top of arbitrary constraint systems, and are declarative. Each program is a logical formula, facilitating reasoning about the models.
HySC has been developed for the construction and analysis of safety-critical embedded hybrid systems. Additionally, it combines several tools like HyTech, FDR, MATLAB, Gnuplot, Graphviz and VVT-RT which are used at different stages of the system development queue: system specification and verification, further the animation and implementation of the system and finally the system test.
This page was last updated October 2004.