Formal methods are not used in their full potential for enhancing software quality in industry. We argue that seamless support in a high-level speci¯cation tool is a viable way to provide system designers with powerful and paradigm speci¯c formal veri¯cation 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 speci¯cations. 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 e®ect of state-space explosion.
The paradigm of rule-based systems is well suited for implementing the behavior
of reactive systems [
Independently of the context of the target system, if a failure of the system
causes a high cost, it must be ensured that such failures can not occur. Using
rules in critical systems implies that the systems behavior must be thoroughly
analyzed. However, analyzing a set of low-level rules is a complex task due to
interactions between rules [
Formal methods are mathematically based methods for specifying and
verifying systems. Developers of complex applications can increase their product and
process quality by utilizing a formal method [
Several CASE tools exists supporting di®erent types of formal methods. The drawback for our purpose is that none of them supports rule-based applications. Modeling the behavior of a rule-based system in, for example, the timed automata veri¯cation tool Uppaal is an error prone and time consuming task since the tool is not designed for modeling rule-based systems.
We address the problem of formally analyzing rule-based applications by
utilizing the power of model-checking for verifying system behavior. A graphical
tool (REX) is constructed [
This paper reports experiences gained from using REX in a case study where an existing industrial system is modeled and veri¯ed. The case-study object is a system for producing assembly plans for engine plants at Volvo IT in SkÄovde, Sweden. The chosen system has a complex behavior dependent on both values of parameters in incoming telegrams and stored values in database tables. The correctness issue of the case-study object is critical since a failure in this system stops the production plants and causes severe economical loss for the company.
The behavior of the system is modeled as a set of rules and complex events
in REX. The correctness of the model is veri¯ed by formulating veri¯cation
expressions in REX that are automatically executed in Uppaal. The results of
our case study shows that using REX as a front-end to Uppaal is a feasible
approach for model-checking a rule-based system of industrial complexity. The
experiences gained from performing the case study teaches us that iteratively
utilizing the ability to formally verify properties of the system during
development is a viable way of coping with the complexity arising in a system built by
interacting rules triggered by complex events. This paper focus on reporting the
lessons learned from the case study, for a detailed description of the actual case
study we refer to [
An event condition action (ECA) rule executes a sequence of code (action A) if a speci¯ed condition C is true when event E occurs. The action part of the rule can be an arbitrary sequence of code and the condition is commonly a boolean expression or an SQL expression returning true or false. The triggering event can be a primitive event, i.e. a single occurrence such as an update of a database, a sensor reading or a message arriving to the system. Additionally, some systems support complex events, implying that the triggering event may be a combination of both primitive and complex events.
Events contributing to a complex event type is composed by operators such as conjunction(^), disjunction (_) and sequence (;). A complex event E = E1 ^ E2, for example, is generated when there is an occurrence of both type E1 and type E2 in the event history. 2.1
REX
The Rule and Event eXplorer (REX) [
Ideally, a model of the system is created in REX to support early detection
of errors in the development phase. Additionally, in the maintenance phase, the
model can be used to ensure that changes in the system, i.e. removing, changing
or adding rules and events, does not cause any undesired side-e®ects.
Specifying models in REX The item types (rules, events, conditions, actions,
dataobjects, data tables) supported by REX are speci¯ed in graphical property
tables. Relations between items of the same type are shown in tree structures
[
In addition to the item types, a scenario editor provides ability to specify di®erent scenarios. A scenario may, for example, be that event E1 occurs at time 2 with event parameter x=4; event E2 occurs at time 4 and event E5 occurs at time 6. In the default scenario, primitive events occur at any time in any order. However, this behavior is likely to cause a state space explosion in the timed automaton model. Providing the user with ability to create scenarios gives the user means to reduce the search space for the model checker and to focus the veri¯cation on speci¯c problems.
ties, such as, "can rule R1 execute before rule R3", are speci¯ed using property
templates. Two useful examples of property templates are Universality and
Existence. The Universality pattern is suitable when checking that the system will
always satisfy a speci¯c property. It is, for example, useful when checking that
a correct ¯nal state will always be reached. The Existence pattern is suitable
when checking if an erroneous state can be reached. Each pattern has a scope,
de¯ning the part of execution when the property must hold. Scope Globally, for
example, de¯nes that the property must hold during the entire execution while
scope P Before Q de¯nes that property P must hold before Q holds [
A property template may, for example be "EXISTS Predicate P BEFORE
predicate Q". The user de¯ned parts of the templates are predicates P,Q,R and
S. In the example, if predicate P="Event E occurs" and predicate Q="Rule R
executes and variable x == 5". Running this property pattern checks whether
event E can occur before rule R executes simultaneously as x == 5. For an
in-depth discussion of how the patterns are used in REX we refer to [
Uppaal
Uppaal is a toolbox for modeling and analyzing speci¯cations built on the theory
of timed automata [
Given an Uppaal model of a system, model-checking can be performed by specifying the properties needed to be checked in timed CTL. The property can quantify over speci¯c states or over a trace of states. It is, for example, possible to ask if variable x will always have a value less than 5 in location S1 in process P (A[]P:S1 and x < 5) or if it is possible to reach location S2 within 3 time units (E <> P:S2 and globalClock < 3). In this paper, Uppaal syntax is used to describe property expressions. 2.3
TUR The group Manufacturing Production Systems at Volvo IT SkÄovde is responsible for development and maintenance of IT solutions, mainly in the areas Supply Chain and Production Planning, for the engine plants in the car factory. The system TUR is implemented and maintained by this group.
The main task of TUR is to convert a high-level assembly plan for items (di®erent types of engines) to be manufactured to a detailed ordered plan for each sub-item (camshaft, crankshaft, etc.) to be constructed or delivered by each assembly-line. The detailed assembly-plan contains an ordered sequence of items to be produced or delivered by each assembly-line.
To avoid lack of items, the assembly plans provided by TUR must be coordinated. The order of items manufactured by di®erent plants must be correlated with each other since assembly lines combining items from di®erent plants must receive all items contributing to their item in correct time and order.
The system TUR is a sequential program with a rule-based semantics. The control °ow of TUR was modeled as rules and complex events in REX. The model created in this project consists of 63 rules, 12 complex events, 50 primitive events, 30 data variables and 45 event parameters separated on di®erent events. Some of the complex events are composed by other complex events in an event hierarchy. One of the complex events with depth three, and four of the complex evens have depth two. The rules are heavily interacting with each other, i.e. the execution of most rules trigger one or several other rules.
Additionally, the speci¯cation consists of 12 modeled database tables with 5 rows ¯lled with values. Moreover, 20 of the actions performed by the rules consist of a function modeling an SQL SELECT expression over one or more of the modeled tables. The veri¯cation of the model was performed by constructing veri¯cation expressions in REX that were automatically executed in the modelchecker provided by Uppaal.
The main problem in verifying TUR was that the behavior of the system to a high degree is dependent on values in database tables. Checking all execution paths with all di®erent combinations of initial database values is an unsolvable problem for any model-checker. A manual analysis were performed to ¯nd a set of initial database states, each representing one of the observable behaviors. The observable behaviors are identi¯ed to be a correct execution with no error message for each possible telegram arriving to the system and di®erent types of error messages that can be reported for each type of telegram. This approach resulted in 20 di®erent initial database states, each of them were checked by 34 di®erent veri¯cation expressions. 3
The experience of using REX for modeling a system larger than toy-size pinpointed abilities of REX that are useful in a tool for developing rules. However, it also revealed some areas where REX can be improved. The following subsections discuss what features a modeling and veri¯cation tool for rule-based system need to support, based on experiences gained from this project. 3.1
The performance of REX and Uppaal is dependent on the level of non-determinism in the model. The non-determinism of the TUR system origins in the fact that the behavior is dependent on values in database tables. The approach taken for overcoming this problem is to trade memory consumption with time. Instead of checking one large non-deterministic model, several rather deterministic models are checked. In the case-study, each model was veri¯ed in less than 1 second. One can argue that reducing the number of checked initial states to 20 is more testing than model-checking. However, the model-checker can still ¯nd erroneous traces that would have been unrevealed by a testing approach although some errors might be uncovered. Since checking for all di®erent initial database states is impossible, one have to put a lot of e®ort in ¯nding a representative set of initial database states in systems like TUR.
The approach with scenarios is a trade o® between time and memory since dividing a speci¯cation into several more deterministic models consumes less memory for checking each model. However, it takes time to run, create and administrate a large set of models. Additionally, some errors may not be reveal if we don't check all possible combinations of initial states.
The behavior of TUR depends on values in database tables, however, the problem with state space explosion is similar for systems where the input to the system is a large number of di®erent events occurring in nondeterministic order. If the number of di®erent events that can occur in any order is n, then the number of orders that must be checker is n!. In REX, preprocessing is performed to analyze the rule set and reduce the number of events in the input domain. The preprocessing complements the approach of trading memory for time. Preprocessing in REX Transforming the entire set of rules from REX to Uppaal will in many cases result in an unnecessarily big automaton. Some of the rules in the rule set will not a®ect the outcome of running the query independently of if they are triggered or not. In order to reduce the search space for the model checker, REX removes rules and events not related to the queried property before transforming the rule set.
Since properties in REX are expressed in terms of rules and events with clearly speci¯ed relations, it is possible to preprocess the model in order to reduce its size. If, for example, property P is de¯ned to check whether rule R1 can be executed before rule R2, only rules and events that can a®ect when R1 or R2 will execute is included in the automaton generated to verify P.
We utilize the knowledge of relations between rules given by the triggering
(TG) and activation (AG) graphs [
Let the set N represent all rules in the rule set and R represent the set of all rules included in property P. The nodes in the triggering and activation graphs are representing the rules in set N. For each node ni 2 N, add all rules representing nodes that can reach ni in TG or AG to the set R. After preprocessing the set of rules and the property to check in REX, the set R contains all rules which directly or transitively triggers or activates some of the rules in the property. All rules in R and all events that may trigger some rule in R are included in the transformed model.
Assume, for example, a set of rules N = fR1; R2; R3; R4; R5; R6g. For i = 1 to 6, each rule Ri 2 N are triggered by an event Ei. The triggering and activation graph of the rule set is shown in Figure 1, ¯lled lines represents triggerings and dashed lines represents activations. Assume that property P = R2 always executes before R1 must be checked and assume a non-deterministic environment where all events E1; E2; E3; E4; E5 and E6 can occur in any order. Checking property P in Uppaal without preprocessing the set of rules results in 6! di®erent occurrence orders for the speci¯ed events. This implies that there are 6! di®erent occurrence orders for Uppaal to check.
If the preprocessor is utilized, the set R initially contains R1 and R2. After preprocessing the rule set, R = fR1; R2; R3g. Hence, if the rule set is preprocessed, the set of rules transformed to Uppaal is reduced to R1; R2; R3 and the environment automaton only consist of E1; E2; E3 resulting in 3! di®erent occurrence orders.
In the case study, the preprocessing did not have a signi¯cant impact of the performance result since the non-determinism mainly originated in data from database tables and not in events occurring in non-deterministic order. However, it may be possible to improve the algorithm for preprocessing rules. If a tuple in a table is never read by any rule in the rules resulting from the preprocessing, it should be possible to remove the table from the rule set before it is transformed to Uppaal and in that way reduce the search space even further. 3.2
Support for veri¯cation is the main aim of the REX tool. The ability to formulate and run veri¯cation questions in every stage of the modeling phase, even when the system is not yet executable, is invaluable when designing a set of rules. The developer need to think very hard about the behavior of the system to be able to formulate veri¯cation expressions and de¯ne expected results. By running the expressions in the veri¯er, the developer retrieves feedback about whether the set of rules behave as intended. If an error is introduced at some stage of development it may be revealed when the veri¯er is executed.
During the case study, the ability to model-check the behavior of the model in Uppaal was repeatedly used. The experience from this approach is that several errors were detected immediately after entering the model. As an example, a new rule R1 was introduced in the model. The action part of R1 generate event E1, E1 triggers rule R2 which is perfectly right. However, E1 is also the initiator of the complex event E3. The fact that E1 initiates E3 was not observer by the developer, but revealed in the model-checker since it found an execution path where rules triggered by E3 could execute in wrong order due to R1.
Lots of research concerning analysis of wether a set of rules is terminating or not exists within the area of active databases [15{17]. However, when a complex system, such as TUR, is modeled where the rules are heavily interacting with each other, guarantees for termination and con°uence is not su±cient. The issue of ensuring that the system behaves as intended requires that application speci¯c properties can be veri¯ed iteratively during development. If veri¯cation is performed for the ¯rst time when the model is ¯nished, the errors may be hard to correct in a rule-based system with interacting rules. The complexity of the behavior of the rule base quickly increases with its size and if the rules are interacting with each other it may be hard to correct an erroneous rule without causing undesirable side-e®ects. 3.3
The simulator in REX uses Uppaal to retrieve step by step information about the execution. Each step is a step of execution in the timed automata representation of the rule set. The information is parsed to rules and events before it is presented to the user. REX supports the ability to exclude single rules and events or groups of rules and events from being visualized in the simulator in order to focus the simulation on speci¯c items. In each step, the user can choose which rule to execute in the next step. Additionally, traces retrieved from executing a veri¯cation expression can be visualized in the simulator.
The simulator in REX provided good support for understanding the behavior of TUR during the case study. However, with the amount of rules that exists in the TUR model, it is hard to follow the behavior of all rules simultaneously. REX shows the state of each rule in each step in a separate color coded swim-lane. The swim-lanes are organized horizontally and scrolling is required to view all rules. The solution is good if the user want to follow the behavior of one or a group of rules, however, it is hard to grasp the behavior of the entire rule set. 4
Most previous work addressing formal analysis of rule based systems concern the properties termination and con°uence (e.g. [15{17]). As far as we know, no previous work addresses model-checking of application speci¯c properties on rules with complex events.
Some previous works exist within the area of visually showing executing
rules (e.g. [
Independently of application area (e.g. Semantic Web, manufacturing, algorithmic trading) analyzing a set of low-level rules is a complex task due to interactions between rules. This paper presents experiences from modeling and verifying a system of industrial complexity as interacting rules using REX. In particular, we have presented our experiences with respect to i) performance, ii) support for automatic veri¯cation and iii) support for simulating rule behavior using a model-checker.
The performance of a rule analysis tool is one of the crucial issues if it is going to be used in practice. Using a model-checker can potentially lead to state space explosion problems. In order to avoid such problems, we have implemented an algorithm that preprocess rule sets.
Automatic veri¯cation of a rule set in every stage of the application development, even when the system is not yet executable, provides support for coping with the complexity of interacting rules.
Simulating rule behavior visually is a good option when verifying a rule set together with domain experts. However, there are no obvious approaches to visualize large rule sets or the entire behavior of a rule set.
We argue that the approach of creating high-level tools to existing formal analysis tools is a viable way of reducing the burden of analyzing ECA rules.
Finally, we believe that automatic veri¯cation of rule sets and simulating rule sets visually desperately need to be integrated with existing software development methods and notations. To the best of our knowledge, many software projects develop ECA rules in ad hoc manners rather than developing ECA rules as a natural component of their software development process.
This work was partially supported by the Swedish Foundation for Strategic Research via the strategic research centre PROGRESS and CUGS (the national graduate school of computer science). The authors would like to thank the sta® at Volvo IT SkÄovde for access to the system TUR and for help and support during this project.