Software engineering and specifications
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 veriﬁcation or on
the application of domain-speciﬁc templates and transformations. We
show how to derive the upper reaches of a family of concurrent garbage
collectors by reﬁnement from a formal speciﬁcation, emphasizing the
application of domain-independent design theories and
transformations. A key contribution is an extension to the classical
lattice-theoretic ﬁxpoint theorems to account for the dynamics of
concurrent mutation and collection.
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.
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.
Abstract 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.
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.
Abstract 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.
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.
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.
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.