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
• DOI: 10.5287/ora-xov2rxgrv
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: CSP; model checking; formal methods; PMCP; formal verification
• Subjects: Communicating Sequential Processes (CSP); Computing; Theory and automated verification; Computer science (mathematics); Communication Sequential Processing (CSP); Model Checking