Generation of Labelled Transition Systems for Alvis Models using Haskell Model Representation.
Marcin Szpyrka, Piotr Matyasik, Michał Wypych · 2013
Abstract. Alvis is a formal modelling language for concurrent systems with the following advantages: a graphical modelling language used to define interconnections among agents, a high level programming language used to define the behaviour of agents and the possibility of a formal model verification. An Alvis model semantics find expression in an LTS graph (labelled transition system). Execution of any language statement is expressed as a transition between formally defined states of such a model. An LTS graph is generated using Haskell representation of an Alvis model and user defined Haskell functions can be used to explore the graph. The paper deals with the problem of translation of an Alvis model into its Haskell representation and discusses possibilities of model verification with the so-called Haskell filtering functions.