Customizable tools for verifying concurrent systems

This dissertation presents a customizable tool framework for the automatic verification of concurrent systems. We identify several fundamental concepts that serve as the building blocks for the extensible tool framework realized in the Concurrency Workbench of North Carolina (CWB-NC) and the Process Algebra Compiler of North Carolina (PAC-NC). The CWB-NC supports a variety of different types of verification and may be easily extended to support new ones. The PAC-NC eases the task of changing the design language supported by the CWB-NC. Given a high-level description of the syntax and semantics of a language, the PAC-NC generates the code necessary to retarget the CWB-NC to the new language. The semantic component of a PAC-NC language description is based on structural operational semantics (SOS) an intuitive yet formal approach to defining the semantics of languages. In order for our framework to be applicable to real-world concurrent systems, which are typically very complex and very big, the code generated by the PAC-NC must be extremely efficient in both time and space. We have therefore focused considerable attention on optimizing PAC-generated code. The PAC-NC has been used to generate CWB-NC front ends for a number of different design languages. The utility of the customizable approach was investigated by applying it to a case study that examined part of a network in a railway signaling system.