During the last 3 years BRICS@Aalborg has been active in
design of hierarchical modelling languages together with implementation of
simulators, verification algorithms and code-generation exploiting the
hierarchical structure. On of our main ambitions is to extend our techniques to
a (backwards compatible) version of the real-time verification tool UPPAAL.
Members
Researcher at BRICS@Aalborg currently working
with hierarchical modelling languages are
Master Theses
A number of
student projects have been aimed at developing verification and simulation
tool for hierarchical modelling languages (in particular in the context of
visualSTATEs hierarchical state/event machines). The following two
projects (hovedfag and speciale) lays the foundation for the final TACA99 and
FMSD publications. The first paper
describes in great detail how to transform a hierarchical model into a flat
one.
The following project extends the compositional technique from reachability
checking to general model checking (wrt modal mu-calculus). The method is
implemented.
A compositional technique for verification of sequential hierarchical
S/E systems. The method is implemented.
A simulator for
StateText:
|
|
Publications
The following publications provides short
descriptions and links to various work we have done during the last couple of
years: The following 3 papers describes a technique which
exploits describes a technique which exploits the hierarchical structure by
reusing already established properties of super-states. The extension of this technique to a timed
setting is far from trivial 2 ,but the technique
certainly provides a promissing starting point.
Design of a hierarchical language for S/E systems with data.
Other
Links
|
|
|
|
|