Two Formal Approaches to Design and Verification of Embedded Rule-Based Systems

摘要

The paper discusses two formal approaches to design and verification of embedded real-time systems incorporating a rule-based system. The first approach is based on a novel visual method of knowledge representation called XTT (extended Tabular Trees), the second one is based on a subclass of coloured Petri nets called D-nets. Both methods use generalized decision rules with non-atomic attribute values. In order to assure reliable and efficient performance, analysis and verification of selected qualitative properties (such as completeness, consistency and optimality) should be carried out. The principal idea consists in integrated design and verification of tabular systems. In both cases, design and verification is supported with computer tools (Mirella and Adder). XML format is used for the interchange of data between those tools.