Automated Abstraction of Labeled Petri Nets
Abstract
Due to the increasing use and complexity of embedded and cyber-physical systems, proper validation of these systems is an increasingly important topic. Because these systems are used in safety-critical situations, even intermittent failures are unacceptable. Formal verification allows for comprehensive validation, but becomes unrealistically complicated for large models. This paper proposes certain transforms to simplify system models without removing any of the details required for verification. These details must be conservative, in that they may not remove any state from the model’s behavior. These transforms have shown this method promising in reducing the complexity of embedded system verification. I.
Type
