Test and Verification

Lecture 3

Subject

Simulation and Verification
Forward Reachability and Compositional Backwards Reachability

Verification in visualSTATE

Codegeneration 

Material

GENERAL

See tutorial on IAR visualSTATE '20 State Test License'.

Look at training material (notes, slides)

VERIFICATION

[SALLT+]

Henrik R. Andersen & Kim G Larsen: Kompositionel og trinvis analyse af tilstandssytemer baseret på afhængighedsanalyse

For the keen reader
J. Lind-Nielsen, H.R. Andersen, G. Behrman, H. Hulgaard, K. Kristoffersen and K.G. Larsen: Verification of Large State/event Systems using Compositionality and Dependency Analysis, In proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 1998, Lecture Notes in Computer Science 1384.

CODE GENERATION

VisualSTATE API Guide
VisualSTATE User Guide
VisualSTATE Quick Start Tutorial

Source Code of the Example
Skeleton of the simpleEventHandler
Complete Example of the CD_Deck

Exercises

Complete the exercises from lecture 2 (see here).

If time permits: Use visualSTATE to generate code for the intelligent light control (exercise 3) and complete it with a simple (text-based) interface (along the lines of the CD_DECK example above).