System Validation

Aim - Modelling a dice game in NuSMV, testing using LTL & CTL, bounded software analysis using CIVL, static and run-time verification using Frama-C.

Implemented a simple dice game model in NuSMV

Tested the model using LTL & CTL constructs

Studied test cases for multiple winners in the game, state space exploration for increasing dice.

Proposed optimizations to the developed model.

Performed bounded software analysis using CIVL

Analyzed segments of code and functions to check for correct code behavior & boundability.

Performed static & run-time verification using Frama-C for different code segments and functions in code.

Recent Posts