Model Checking Systems with Replicated Components using CSP

Thesis

The Parameterised Model Checking Problem asks whether an implementation Impl(t) satisfies a specification Spec(t) for all instantiations of parameter t. In general, t can determine numerous entities: the number of processes used in a network, the type of data, the capacities of buffers, etc. The main theme of this thesis is automation of uniform verification of a subclass of PMCP with the parameter of the first kind, using techniques based on counter abstraction. Counter abstraction works ...

Expand abstract

Authors: Mazur, T

• Publication date: 2011
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: CSP; model checking; formal verification; PMCP; formal methods
• Subjects: Computer science (mathematics); Model Checking; Communicating Sequential Processes (CSP); Communication Sequential Processing (CSP); Theory and automated verification; Computing