Systems Engineering: A Formal Approach. Part 4. Analysis Methods

摘要

There are several methods to analyze a model. To verify invariant properties there are two kinds of invariant methods: place invariants and transition invariants. Place invariants can be used to prove properties that hold in each reachable state. A transition invariant is a characterization of (finite) traces that bring an actor back to its initial state or an equivalent one. These methods are studied in the first section. The second section considers occurrence graph methods. They are used to check if a system can reach states with certain properties. These methods are specialized in section three to study the time behavior of systems, specifically to compute throughput or response times.