Overview
Runtime verification is a lightweight approach to program reliability. Its basic idea is to gather information during program execution and use it to conclude properties about the program, either during testing or in operation, which increases the confidence in whether the program implementation conforms to its specifications.
UIMDRIVER standing for UML Interaction Model Driven Runtime Verifier, is a runtime verification tool for JAVA programs. It introduces UML2.0 interaction overview diagrams and sequence diagrams to construct simple but expressive scenario-based specifications, and takes an runtime verification approach to check the consistency between JAVA programs and their specifications. It is able to perform two types of consistency checking: exceptional consistency checking and mandatory consistency checking. The exceptional consistency requires that any forbidden scenario described by a given interaction overview diagram never happens during the execution of a program, and the mandatory consistency requires that if a reference scenario described by a given sequence diagram occurs during the execution of a program, it must immediately adhere to a scenario described by a given interaction overview diagram.
The tool can check four types of specifications:
Exceptional consistency specifications require that any forbidden scenario described by a given interaction overview diagram D never happens during the execution of a program;
Forward mandatory consistency specifications require that if a reference scenario described by a given sequence diagram D occurs during the execution of a program, then a scenario described by a given interaction overview diagram G must follow immediately;
Backward mandatory consistency specifications require that if a reference scenario described by a given sequence diagram D occurs during the execution of a program, then it must follow immediately from a scenario described by a given interaction overview diagram G;
Bidirectional mandatory consistency specfications require that if a reference scenario described by a given sequence diagram D1 occurs during the execution of a program and another reference scenario described by another given sequence diagram D2 follows, then in between these two scenarios, a scenario described by a given interaction overview diagram G must occur exactly.
Figure 1: Scenario-based specifications
Download
The tool is available now! You may download it via the download page.
|