Logotype Mälardalen University

MRTC publications



Verification of an industrial rule-based manufacturing system using REX

Full text:  
Authors: AnneMarie Ericsson (University of Skövde), Mikael Berndtsson (University of Skövde), Paul Pettersson, Lena Pettersson (Volvo Information Technology, Skövde)
Source: 1st International Workshop on Complex Event Processing for Future Internet
 

Abstract

Formal methods are not used in their full potential for enhancing software quality in industry. We argue that seamless support in a high-level specification tool is a viable way to provide system designers with powerful and paradigm specific formal verification techniques. Event condition action (ECA) rules can be used to model and implement reactive behavior in, for example, the semantic web. Independently of target system, the behavior of rule-based systems are known to be hard to analyze. The REX tool is a rule-based front-end to the timed automata CASE-tool Uppaal. The model-checker in Uppaal is used by REX enabling seamless support for model-checking rule-based specifications. This paper presents experiences from modeling and verifying a system of industrial complexity as interacting rules using REX. We conclude that repeatedly performing formal analysis when constructing a system with interacting rules is a viable way of coping with the complexity of the model. Additionally, we present an implemented algorithm for optimizing the model to reduce the effect of state-space explosion.
 

BibTeX entry

@inproceedings{Ericsson_1541:2008,
   author = {AnneMarie Ericsson and Mikael Berndtsson and Paul Pettersson and Lena Pettersson},
   title = {Verification of an industrial rule-based manufacturing system using REX},
   booktitle = {1st International Workshop on Complex Event Processing for Future Internet},
   month = {September},
   year = {2008},
   url = {http://www.mrtc.mdh.se/index.php?choice=publications&id=1541},
}

  • Mälardalen University |
  • Box 883 |
  • 721 23 Västerås/Eskilstuna |
  • 021-101300, 016-153600 |
  • webmaster |
  • Latest update: 2010.05.10