Design and Verification of Rule-Based Systems for Alvis Models

Abstract

Alvis is a modelling language designed for embedded systems that provides a possibility of a formal model verification. Because of the fact that many embedded systems contain a rule-based system as a part of them, it is necessary to provide a possibility to include such systems into Alvis models. Alvis combines flexible graphical modelling of interconnections among agents with a high level programming language used for the description of agents behaviour. The most natural way of including a rule-based system into an Alvis model is to encode it in the Haskell functional language. Some Haskell features like lazy evaluation, pattern matching, high level functions etc. make it a very attractive proposition from the rule-based systems' engineering point of view. The paper presents a method of encoding and verification of rule-based systems with Haskell to include them into Alvis models. © Springer-Verlag Berlin Heidelberg 2013.