Modal transition systems are specification languages that allow the expression of loose specifications. They can model a development process where an initially partial specification is stepwise refined until an implementation is obtained. We propose to generalize modal transition systems to a nominal setting to facilitate the handling of names and binders as encountered in name-passing process calculi. We need to show compositionality of the refinement relation. Beyond that we want to further generalize this idea by compiling SOS rule formats that ensure compositionality. The results of this research should give a general specification language where proofs of the theory carry over to other process calculi expressible in our framework.
In the networked world of today, concurrent communicating systems are
ubiquitous. As such systems are complex, we need formal methods to reason about
their properties. When developing software we want to start with a specification
of the intended behavior of the system that we can later use to check whether our
implementation meets the requirements. Process calculi [
With process calculi, the languages for specification and implementation of a system are the same. Bisimulation is used to check the correctness of an implementation according to a specification. As bisimulation is an equivalence, this limits the set of possible implementations to a single equivalence class. This means that contrary to a real-world development process all behavior must already be defined in the initial specification. Furthermore for the specification of a system composed of several components it is necessary to specify all behavior of the components, even the behavior that is only internally visible. We want to describe a development process where it is possible to refine the specification of a system by refining the specification of one of its components, as illustrated in Figure 1. ? Initial stage of research, supervised by Joachim Parrow
Modal transition systems [
Name-passing process calculi such as the Pi calculus [
An important property of a specification language is compositionality: The
problem of checking the correctness of a complete system according to a
specification should be decomposable into the simpler problems of checking correctness
of the components. For process calculi, bisimulation preserved by the process
operators fulfills compositionality [
The area of specification languages is large and there are many papers
introducing new languages. Each time the underlying theory such as compositionality
has to be proved again. Rule formats [
The process calculus concept was first introduced by Milner in his work on the
Calculus of Communicating Systems [
In [
Process calculi and specification languages rely on the concepts of names and
binders. Pitts introduced nominal logic [
For process calculi where terms are elements of arbitrary nominal sets Parrow
et al. [
Structural operational semantics (SOS) was first presented by Plotkin in [14]
as a structured method to define rules for operational semantics. The idea was
widely adopted and extended by the concept of rule formats [
We propose to combine the concepts of modal transition systems and nominal logic to define a specification language that improves the handling of names and binders as used in name-passing process calculi. This will give us the flexibility of modal transition systems on top of a rigorous theory for reasoning about objects depending on names. It will allow the expression of the behavior of a system in the style of name-passing process algebras while facilitating the refinement of its specification through the use of may and must transitions as found in modal transition systems. We need to define a refinement relation and prove compositionality with the parallel and other process operators. Furthermore we propose to generalize our specification language by finding SOS rule formats such that compositionality holds. We will find encodings of existing process algebras into instances of our rules, eliminating the need to repeat the proofs in each expressible instance.
To increase the confidence in our proofs we will formalize part of our theory in the interactive theorem prover Isabelle. In particular, we will rely on the definitional extension Nominal Isabelle, providing convenient measures of handling names and binders. 4
My research on this topic is still in the initial stage. I have conducted a literature survey on process calculi and modal transition systems. In earlier work I gained experience with proofs on properties of bisimulation, notably in a nominal setting. Furthermore, I have had some practice in formalizing proofs in Nominal Isabelle. 5
The expected contributions of this research are as follows: – definition of a specification language using nominal transition systems with modal may and must transitions, a satisfaction relation and a notion of refinement that allows composition with logical and process operators, – proofs that our specification language fulfills compositionality with operators such as the parallel operator and comparisons of our refinement relation with existing forms of bisimulation, – methods for checking refinement of specifications, – generalization of the concept through rule formats that ensure compositionality, – applications of our framework by means of encodings of existing process algebras1, – formalization of some of the proofs in the interactive theorem prover Isabelle.
This research will generalize nominal process algebras to allow the expression of loose specifications that can be refined stepwise. Our specification language will simplify the task of verification for systems that are composed of several 1 exactly which process algebras is not set yet components because of compositionality: It will permit to check the correctness of a refinement step by reducing the test to a correctness check of the refined component. Furthermore, by describing a set of rule formats that ensure compositionality this research will be applicable to various existing process algebras while the desired properties need to be proved only once in the general framework. The proofs written in the theorem prover Isabelle can be reused for process algebras that can be expressed as instances of our rule formats. 6
A large part of this research will deal with the theoretical reasoning about features of our proposed rule formats for nominal modal transition systems. To validate that our framework meets the requirements, we will give proofs for the desired properties such as compositionality. We will formalize part of our proofs in Nominal Isabelle to achieve a high confidence in their correctness. Furthermore we will investigate how our specification language can be used in combination with existing tools for model checking.
The advantage of our modal specification language with refinement over approaches using bisimulation can be assessed through performance tests of tools that verify the correctness of an implementation according to a specification when components of a partial implementation are refined. As for the general framework of rule formats we will evaluate its usefulness by encoding existing process calculi in it. For the process calculi we can encode this way the theoretical results will carry over, eliminating the need for new proofs for every expressible calculus. 7
Currently I am taking a course on interactive theorem proving in Isabelle to increase my knowledge in that area. Moreover, I am taking a course on category theory that is expected to help with the understanding of papers that use category theory as a means of reasoning about rule formats. As a next step I will conduct a literature survey on structural operational semantics for nominal process algebras. In Swedish universities it is common to write a thesis for a Licentiate degree after completion of half of the studies for a PhD. In this thesis I plan to include the definition of a nominal modal specification language, proofs of its properties such as compositionality, methods for refinement checking and the formalization of the definitions in Nominal Isabelle, due by fall 2018. Subsequently I will work on generalizing the results through rule formats, applications and further formal proofs in Nominal Isabelle for inclusion into the PhD thesis. I expect to finish in 2021.