2010
Formal derivation of concurrent garbage collectors
with Peter Pepper and Douglas R. Smith
Concurrent garbage collectors are notoriously difficult to implement correctly. Previous approaches to the issue of producing correct collectors have mainly been based on posit-and-prove verfication or on the application of domain-specfic templates and transformations. We show how to derive the upper reaches of a family of concurrent garbage collectors by refinement from a formal specfication, emphasizing the application of domain-independent design theories and transformations. A key contribution is an extension to the classical lattice-theoretic fixpoint theorems to account for the dynamics of concurrent mutation and collection.
2008
Evolving specification engineering
with Peter Pepper and Douglas R. Smith
The motivation for this work is to support a natural separation of concerns during formal system development. In a development-by-refinement context, we would like to be able to first treat basic functionality and normal-case behavior, and then later add in complicating factors such as physical limitations (memory, time, bandwidth, hardware reliability, and so on) and security concerns. Handling these complicating factors often does not result in a refinement, since safety or liveness properties may not be preserved. We extend our earlier work on evolving specifications (1) to allow the preservation of both safety and liveness properties under refinement, and (2) to explore a more general notion of refinement morphism to express the introduction of complicating factors.
2006
Deriving secure network protocols for enterprise services architectures — with Matthias Anlauff and Asuman Suenbuel
Abstract
Enterprise Service Architectures are emerging as a promising way to compose Web-Services as defined by the W3C consortium, to form complex, enterprise level services. However, due to the fact that each Web-Service composition is also a protocol composition, this composition gets problematic, if security protocol mechanisms are used for the individual Web-Services, because security properties are not preserved under composition. This paper outlines the derivational approach, that on the one hand mimics the general engineering practice when combining security features, but on the other hand avoids the problems that can arise during the composition of Web-Services by using well-founded mathematical concepts. The Protocol Derivation Assistant, a tool that supports this approach, is also briefly described.
2003
Colimits for concurrent collectors
with Peter Pepper and Douglas R. Smith
This case study applies techniques of formal program development by specification refinement and composition to the problem of concurrent garbage collection. While the specification formalism is mainly based on declarative programming paradigms, the imperative aspect is dealt with using monads. We also outline the use of temporal logic in connection with monadic specifications.
Software development by refinement
with Douglas R. Smith
This paper presents an overview of the technical foundations and current directions of Kestrel Institute’s approach to mechanizing software development. The approach emphasizes machine-supported refinement of property-oriented specifications to code, based on a category of higher order specifications. A key idea is representing knowledge about programming concepts, such as algorithm design, and datatype refinement by means of taxonomies of abstract design theories and refinements. Concrete refinements are generated by composing library refinements with a specification.
The framework is partially implemented in the research systems Specware, Designware, Epoxi, and Planware. Specware provides basic support for composing specifications and refinements via colimit, and for generating code via logic morphisms. Specware is intended to be general-purpose and has found use in industrial settings. Designware extends Specware with taxonomies of software design theories and support for constructing refinements from them. Epoxi builds on Designware to support the specification and refinement of systems. Planware transforms behavioral models of tasks and resources into high-performance scheduling algorithms. A few applications of these systems are presented.
2002
Guarded transitions in evolving specifications
— with Douglas R. Smith
We represent state machines in the category of specifications, where assignment statements correspond exactly to interpretations between theories. However, the guards on an assignment require a special construction. In this paper we raise guards to the same level as assignments by treating each as a distinct category over a shared set of objects. A guarded assignment is represented as a pair of arrows, a guard arrow and an assignment arrow. We give a general construction for combining arrows over a factorization system, and show its specialization to the category of specifications. This construction allows us to define the fine structure of state machine morphisms with respect to guards. Guards define the flow of control in a computation, and how they may be translated under refinement is central to the formal treatment of safety, liveness, concurrency, and determinism.
2001
Composition and refinement of behavioral specifications
with Douglas R. Smith
This paper presents a mechanizable framework for specifying, developing, and reasoning about complex systems. The framework combines features from algebraic specifications, abstract state machines, and refinement calculus, all couched in a categorical setting. In particular, we show how to extend algebraic specifications to evolving specifications (especs) in such a way that composition and refinement operations extend to capture the dynamics of evolving, adaptive, and self-adaptive software development, while remaining efficiently computable. The framework is partially implemented in the Epoxi system.
Towards semantics of self-adaptive software
When people perform computations, they routinely monitor their results, and try to adapt and improve their algorithms when a need arises. The idea of self-adaptive software is to implement this common facility of human mind within the framework of the standard logical methods of software engineering. The ubiquitous practice of testing, debugging and improving programs at the design time should be automated, and established as a continuing run time routine.
Technically, the task thus requires combining functionalities of automated software development tools and of runtime environments. Such combinations lead not just to challenging engineering problems, but also to novel theoretical questions. Formal methods are needed, and the standard techniques do not suffice.
As a first contribution in this direction, we present a basic mathematical framework suitable for describing self-adaptive software at a high level of semantical abstraction. A static view leads to a structure akin to the Chu construction. An dynamic view is given by a coalgebraic presentation of adaptive transducers.
1999
Semantics of first order parametric specifications
Parametricity is one of the most effective ways to achieve compositionality and reuse in software development. Parametric specifications have been thoroughly analyzed in the algebraic setting and are by now a standard part of most software development toolkits. However, an effort towards classifying, specifying and refining algorithmic theories, rather than mere datatypes, quickly leads beyond the realm of algebra, and often to full first order theories. We extend standard semantics of parametric specifications to this more general setting.
The familiar semantic characterization of parametricity in the algebraic case is expressed in terms of the free functor, i.e. using the initial models. In the general case, the initial models may not exist, and the free functor is not available. Various syntactic, semantic and abstract definitions of parametricity have been offered, but their exact relationships are often unclear. Using the methods of categorical model theory, we establish the equivalence of two well known, yet so far unrelated definitions of parametricity, one syntactic, one semantic. Besides providing support for both underlying views, and a way for aligning the systems based on each of them, the offered general analysis and its formalism open up several avenues for future research and applications.