Rule Invariants in Graph Transformation Systems for Analyzing Safety-Critical Systems
Automating software engineering activities for developing safety-critical systems reliably and correctly brings along the challenge to combine expressive specification methods with powerful analysis techniques. The focus of this paper lies in the analysis of graph transformation systems by analysis techniques transferred from Petri nets. Since Petri nets are famous for their powerful analysis techniques we have started to transfer several notions from Petri nets to graph transformation systems. Especially, invariants provide vast possibilities for investigating a model. Hence, we have transferred transition invariants to rule invariants in graph transformation systems. Moreover, we have given a characterization of rule invariants. Due to the greater expressiveness of graph transformation this characterization is more complex than the one of transition invariants. The main fact about transition invariants is recaptured for rule invariants. Therefore, suitable Petri net notions like reachability, liveness, and boundedness are transferred to graph transformation systems. This allows a suitable analysis of graph transformation systems as is exemplified by a safety-critical system specification in the area of human-computer interaction. After a presentation of a graph grammar specifying a safety-critical system concerning interaction on the flight deck of an aircraft several notions of Petri nets are transferred to graph transformation systems. The corresponding notions concerning graph transformation systems are then demonstrated using the safety-critical example.
Dieser Eintrag ist freigegeben.