Phase 3: Specification and Model Checking

Objectives

This phase of the project is designed to apply a formal (mathematical) modeling and verification technique to a part of our ongoing case study:

• apply mathematical modeling to capture the core behavior of the WhatsUpGU server,

• apply simulation to gain insight on some of its basic behavior,

• specify some of its correctness properties in a temporal logic, and

• apply model checking to verify the properties of the modeled behavior.

General Description

The subject of this phase is to mathematically model the core functionality of the WhatsUpGU server, specify its correctness properties and prove, using model checking, that all properties are satisfied by the model. To this end, you make network of timed automata capturing the basic functionality of the server and its concurrent behavior with respect to user requests. To make the model finite and manageable, we assume that there are 2 users and can send each other at most 2 messages and message types. We represent both the users and the message with constants 0 and 1. To do this we model the following functionality:

• adding a message,
• editing a message,
• deleting a message,
• fetching messages one by one, and
• fetching complete.

Also, you model 2 users that can perform the above-mentioned operations in any sensible order. In addition you phrase 5 most important properties about its behavior and verify it on the developed model.

Deliverables

The deliverable for this phase consists of a single zip file with two folders: a folder containing a single pdf file of the report and another folder containing all Uppaal models, queries (properties) and simulation traces. This phase is organized into 2 sections.

Modeling and Simulation in Uppaal

After finishing your modeling try the test scenarios you have designed in your integration testing (Phase 2); save these traces and include them as an appendix to your report. If any of the scenarios fail in your simulation, redesign your model to make the simulation trace possible. Document all major changes you made. In your final report present both the initial and the final model and report in a step-wise manner the changes leading to the final model.

Specifying and Model Checking Properties

Specify at least 5 properties that you expect from the server behavior. Examples of such properties are the following:

• The server should never deadlock,
• If a user deletes a message and does not add it again, the message will not appear when fetch is performed.

Include these properties in your final report.

Translate these messages into the temporal logic language of Uppaal. In some cases you may need to design monitor automata to make the coding feasible / more straightforward. Discuss the properties (and their monitor automata) with the instructors before you proceed with the next step. Document your temporal logic formulae after that you discuss them with the instructor; include both the formulae and the monitor automata and sufficient explanation to show that they reflect the intuitive properties.

Then proceed with model checking the properties. In case you find a counter-example, correct the model (or the property) until all properties are verified correct. In case of any major changes in the model or property, document and explain the counter-examples witnessing the initially incorrect design and the changes leading to a correct model. In case you change a model to satisfy property, verify all previous properties to make sure that you have not invalidated them.