 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights | |||||||||||||||||||||||||||
| Wissensbrowser starten | |||||||||||||||||||||||||||
| |||||||||||||||||||||||||||
| |||||||||||||||||||||||||||
|
| ||||||
|  | | | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Erfahrung |
|
The UML Verification Environment II |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung der Erfahrung | |||||||||
| |||||||||
| To obtain the static structure and the dynamic behaviour of a UML model UVE onsiders class diagrams and state-machine diagrams. All other diagrams are gnored. The action language for state-machine annotations and method implementations is a subset of C++. Dynamic creation, deletion, and recreation of objects is supported if the number of objects alive at a single point in time is bounded by a user-given limit.
In class diagrams, UVE supports polymorphism (single inheritance and virtual methods) and bounded associations, aggregations, and compositions. Currently not supported are multiple inheritance and template classes. In state-machine diagrams, UVE allows hierarchical state-machines, and- and or-states, triggered operations, and pseudo-states. Further supported are parameterised events and event hierarchies by inheritance. Time events and event deferring are currently not allowed; event queues have to be statically bounded. Recursion and loops are accepted when statically bounded. Integer, boolean, and pointer-to-object are allowed as types; oating-point values, arrays, and general pointers are not supported. Note that this enumeration refers to the capabilities of UVE at time of conducting the case study. In the meantime UVE has further evolved, e.g. it supports arrays in the current version and there are efforts to support infinite UML-Models in UVE1. UVE is more appropriate for this case study than other tools, e.g. like ObjectCheck2, since it supports a larger subset of UML, e.g. enhanced object oriented features like virtual methods and triggered operations, and a more convenient state-machine language comprising composite states. To The Sensor Voting UML Model I Back to overview Formal Verification of a Sensor Voting and Monitoring UML Model | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
| ||||
| ||||
| The UML Verification... | ||||
| ||||
| ||||
| ||||
| ||||
| Literaturhinweise | | ||
| ||||
|
| | ||
|
| | ||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
