Part 3, Project

Modeling

Think of a concrete scenario that has (possibly conflicting) safety and security properties. Brainstorm a bit in your group about what interest you the most.

Create an informal model and description first, then choose some key components and model them formally in NuSMV.

Ideas for possible models

As much as possible, use your own idea! It can be something from your everyday life or a futuristic next-generation system.

Modeling key features and properties

For some key functionality and properties for your scenario, create a model in NuSMV.

The model should have at least the following modules:

1. Modules for each key component.
2. A user module that models possible choices of a (benign or malicious) user.
3. A main module that ties everything together.

Write at least five properties, out of which at least one must be a liveness property.

Verify your model with NuSMV and ensure that the properties are verified as correct.

Apply a validation technique to your model and assess whether you think the properties themselves are right.

Deliverables

1. Upload a short presentation (about 2–3 slides) giving an informal overview of your project.
   Try to use a few diagrams to show the project and how you model it.
2. Upload the resulting NuSMV model and description (either as a comment, or as a separate file or text input).