Keywords: Type Theory, Higher Order Logic, Verification, Specification, Concurrent Systems/Algorithms, Temporal Logic, Petri nets, UNITY
The objective of this project is to explore the use of an expressive higher-order logic with dependent types to develop a library of mathematical concepts that are useful for specification and verification of concurrent and distributed systems. The library should support a strongly typed specification and verification style which as pointed out by Lamport is known to be difficult to achieve in program and system verification. Furthermore, the notion of system should be as general as possible and should cover software artifacts such distributed algorithms as well as hardware such as asynchronous circuits. The particular emphasis is on systems that exhibit real concurrency.
As a starting point we have chosen to use the original UNITY methodology which since its introduction in 1988 by Chandy and Misra is one of the most elegant and formally tractable formalisms that still receives continuing interest by many researchers.
As a first step we have conducted a formalization of UNITY in the Calculus of Inductive Constructions which gives not only the UNITY methodology a rigorous formal status but it also combines the advantages of a type theory with dependent types with the UNITY language. Instead of UNITY we have used the more recent New UNITY proposal, which does not deviate from UNITY essentially but is conceptually more elegant.
The next step in this project was generalizing the approach from UNITY programs to arbitrary labelled transition systems. Labelled transition systems are of interest, since virtually each formalism for system specification can be at least equipped with an abstract transition system semantics. In fact for many formalisms labelled transition systems constitute the main semantics. In addition to the use of a more general notion of system we have generalized the original notion of unconditional fairness that is imposed on UNITY programs to a much more general notion of (selective) group fairness.
As a particular model we are currently exploring the application of our general approach to Petri nets, the historically first model for concurrent systems proposed by http://www2.informatik.uni-hamburg.de/tgi/mitarbeiter/profs/petri_eng.html. More precisely, we are interested not only in the basic Petri net model but in high-level Petri net models such as coloured nets that can model flow of arbitrarily complex data objects instead of indistinguishable tokens only. An even more powerful generalization of Petri nets that is of recent intrest is rewriting logic , and indeed this is one of the formalisms that could serve as another intersting application of UNITY style temporal logic in its generalized form.
From a more theoretical point of view the formalization of UNITY and its generalization is also interesting as a case study in the use of the Calculus of Inductive Constructions for metalogical reasoning. We give formal verifications of all UNITY proof rules on a proof-theoretic level which is independent of a particular execution semantics. Furthermore, we prove a compositionality result for UNITY logic which is actually a new application of the Curry-Howard isomorphism.
Of course, due to the vast amount of formal detail it is impossible to engage in such a project without a mature tool. We have used the COQ proof assistant for the entire development. The sources of the formalization of UNITY are available below. The generalized version of UNITY will be available in the near future.
Relevant References: