View Source Document

Chris Pressey.md

Commentary by Chris Pressey

This work is distributed under a CC-BY-ND-4.0 license, with the following explicit exception: the ratings may be freely used for any purpose with no limitations.

Model Checking

Model Checking CTL is Almost Always Inherently Sequential

By "inherently sequential" they mean P-complete. Model checking for CTL is already known to be P-complete, but they show it for a whole bunch of different fragments too.

Cycle Detection in Computation Tree Logic

A variation of CTL which is aware of cycles is defined; it is called Cycle-CTL. Various things are proven about Cycle-CTL*. It is a very expressive language for statements about the temporal behaviour of a system.

Direct Model-checking of SysML Models

SysML models are normally model-checked by first translating them to UPPAAL. The authors extend a tool that works with (extended) SysML models (TTool) to make it run model-checking directly on the SysML model.

The basic theory behind model-checking is straightforward: it's testing reachability (whether one node is reachable from another, in a graph). This is apparent when you look at algorithms for, e.g. model-checking CTL and the modal mu-Calculus.

The complexities in implementation come from making this efficient, because in the worst case there will be a combinatorial explosion when constructing the graph. The authors discuss some steps they took to address this.

Their extended version of SysML supports timing, so part of the model involves summing durations and comparing times.

An interesting observation, from section 6.2:

For some properties, such as liveness, we noticed that a DFS exploration is generally more effective than a BFS one as the main proof of unsatisfiability is given by loops or deadlocks. A search in depth increases the odds to find quickly those features.

Lecture Notes on CTL Model Checking

.

multi tasking - Help understanding Petersons Algorithm for N Processes - Computer Science Stack Exchange

The answerer gives a Promela model for the algorithm

Sally by SRI-CSL

.

The Omega Library Interface Guide

.

Getting started with SMV

.