We present an algebra of discrete timed input/output automata that may execute in the context of different clock granularities – which we call timed machines; this algebra includes a refinement operator through which a machine can be extended with new states and transitions in order to accommodate a finer clock granularity as required to interoperate with other machines, and an extension of the traditional product of timed input–output automata to the situation in which the granularities of the two machines are not the same. Over this algebra, we then define an algebra of networks of timed machines that includes operations through which networks can be modified at run time, thus offering a model for systems of interconnected components that can dynamically bind to other systems and, therefore, cannot be adjusted at design time to ensure that they operate in a timed homogeneous setting. We investigate important properties of timed machines such as consistency – in the sense that a machine can be ensured to generate a non-empty language, and feasibility – in the sense that a machine can be ensured to generate a non-empty language no matter what inputs it receives, and propose techniques for checking if timed machines are consistent or are feasible. We generalise those properties to networks of timed machines, and investigate how consistency and feasibility of networks can be proved through properties that can be checked at design time without having to compute, at run time, the product of the machines that operate on those networks, which would not be practical.

We propose a logic-independent approach to logic programming through which the paradigm as we know it for Horn-clause logic can be explored for other formalisms. Our investigation is based on abstractions of notions such as logic program, clause, query, solution and computed answer, which we develop over Goguen and Burstall's theory of institutions. These give rise to a series of concepts that formalize the interplay between the denotational and the operational semantics of logic programming. We examine properties concerning the satisfaction of quantified sentences, discuss a variant of Herbrand's theorem that is not limited in scope to any particular logical system or construction of logic programs, and describe a general resolution-based procedure for computing solutions to queries. We prove that this procedure is sound; moreover, under additional hypotheses that reflect faithfully properties of actual logic-programming languages, we show that it is also complete.

More than a decade has passed since Herbrand’s theorem was first generalized to arbitrary institutions, enabling in this way the development of the logic-programming paradigm over formalisms beyond the conventional framework of relational first-order logic. Despite the mild assumptions of the original theory, recent developments have shown that the institution-based approach cannot capture constructions that arise when service-oriented computing is presented as a form of logic programming, thus prompting the need for a new perspective on Herbrand’s theorem founded instead upon a concept of generalized substitution system. In this paper, we formalize the connection between the institution- and the substitution-system-based approach to logic programming by investigating a number of features of institutions, like the existence of a quantification space or of representable substitutions, under which they give rise to suitable generalized substitution systems. Building on these results, we further show how the original institution independent versions of Herbrand’s theorem can be obtained as concrete instances of a more general result.

No abstract available.

We present a research agenda on an emerging topic in software engineering, namely the synergy between Software Product Line Engineering (SPLE) and Service-Oriented Computing (SOC). Our proposal is to develop rigorous modelling techniques as well as analysis and verification support tools for assisting organisations to plan, optimise, and control the quality of 'software service' provision, both at design time and at run time. We foresee a flexible engineering methodology according to which 'software service line organisations' can develop novel classes of service-oriented applications that can easily be adapted to customer requirements as well as to changes in the context in which, and while, they execute. By superposing variability mechanisms on current languages for service engineering, based on policies and strategies defined by service providers, we envision the possibility of identifying variability points that can be triggered at run time to increase adaptability and optimise the (re)use of resources.

Abstract We propose a formal operational semantics for service discovery and binding. This semantics is based on a graph-based representation of the configuration of global computers typed by business activities. Business activities execute distributed workflows that can trigger, at run time, the discovery, ranking and selection of services to which they bind, thus reconfiguring the workflows that they execute. Discovery, ranking and selection are based on compliance with required business and interaction protocols and optimisation of quality-of-service constraints. Binding and reconfiguration are captured as algebraic operations on configuration graphs. We also discuss the methodological implications that this model framework has on software engineering using a typical travel-booking scenario. To the best of our knowledge, our approach is the first to provide a clear separation between service computation and discovery/instantiation/binding, and to offer a formal framework that is independent of the SOA middleware components that act as service registries or brokers, and the protocols through which bindings and invocations are performed.

No abstract available.

We discuss the suitability of service-oriented computing for the automotive domain. We present a formal high-level language in which complex automotive activities can be modelled in terms of components and services that can either be provided by the on-board system or procured from external providers (e.g. via the web) through a negotiation process that involves quality of service attributes and constraints. The ability to re-configure activities, in real-time, through service discovery and dynamic binding takes us one step further from current component-based development techniques: it enhances flexibility and adaptability to changes that occur in the environment in which the system operates (driver, automobile, and external circumstances) and, ultimately, leads to improved levels of satisfaction, safety and reliability.

We propose a mathematical semantics for event-based architectures that serves two main purposes: to characterise the modularisation properties that result from the algebraic structures induced on systems by this discipline of coordination; and to further validate and extend the categorical approach to architectural modelling that we have been building around the language CommUnity with the ‘implicit invocation’, also known as ‘publish/subscribe’ architectural style. We then use this formalisation to bring together synchronous and asynchronous interactions within the same modelling approach. We see this effort as a first step towards a form of engineering of architectural styles. Our approach adopts transition systems extended with events as a mathematical model of implicit invocation, and a family of logics that support abstract levels of modelling.

This paper proposes the development of a logic for verifying properties of programs in rewriting logic. Rewriting logic is primarily a logic of change, in which deduction corresponds directly to computation, and not a logic to talk about change in a more indirect and global manner, such as the different modal and temporal logics that can be found in the literature. We start by defining a modal action logic (VLRL) in which rewrite rules are captured as actions. The main novelty of this logic is a topological modality associated with state constructors that allows us to reason about the structure of states, stating that the current state can be decomposed into regions satisfying certain properties. Then, on top of the modal logic, we define a temporal logic for reasoning about properties of the computations generated from rewrite theories, and demonstrate its potential by means of several examples.

Community is a formal approach to software architecture. Its main characteristics are: a precise, yet intuitive mathematical semantics based on categorical diagrams; a clear separation between computation, coordination, and distribution (including mobility); and a simple state-based language, inspired by Unity, to describe behaviour. This paper discusses the applicability of this approach to location-aware systems through the modelling of the GSM handover protocol, namely the way communication with a moving cellular phone passes from one station to another. The case study was developed with the Community Workbench, a tool that animates distributed and mobile architectural models.

Abstract. The traditional notion of superposition has been used for supporting two distinct aspects of parallel program design: composition and refinement. This is because, when trace-based semantics of concurrency are considered, which is typical of most formal methods, these two relationships are modelled as inclusion between sets of behaviours. However, when forms of non-deterministic behaviour have to be considered, which is the case for component and service-based development, these two aspects do not coincide. In this paper, we show how the two roles of superposition can be separated and supported at the language and semantic levels. For this purpose, we use a categorical formalisation of program design in the language CommUnity that we are also using for addressing architectural concerns, another area in which the distinction between composition and refinement is particularly important.

We develop a notion of higher-order connector towards supporting the systematic construction of architectural connectors for software design. A higher-order connector takes connectors as parameters and allows for services such as security protocols and fault-tolerance mechanisms to be superposed over the interactions that are handled by the connectors passed as actual arguments. The notion is first illustrated over CommUnity, a parallel program design language that we have been using for formalizing aspects of architectural design. A formal, algebraic semantics is then presented which is independent of any Architectural Description Language. Finally, we discuss how our results can impact software design methods and tools.

No abstract available.

In this paper, we address the integration of a distribution dimension in an architectural approach to system development and evolution based on the separation between coordination and computation. This third dimension allows us to separate key concerns raised by mobility, thus contributing to our ability to handle the complexity that is inherent to systems required to operate in "Internet time and space".

Abstract We present methodological and technological solutions for evolving large‐scale software systems. These solutions are based on many years of research and experience in developing systems in one of the most volatile application domains—banking. We discuss why ‘promising’ software development techniques, such as object‐oriented and component‐based approaches, on their own, cannot meet the challenges and objectives of software development today, and propose a three‐layered architectural approach based on the strict separation between computation, coordination and configuration. We present a set of modelling primitives, design principles and support tools through which such an approach can be put effectively into practice, and discuss how it promotes a more ‘dynamic’ approach to software evolution. Finally, we make comparisons with related work. Copyright © 2002 John Wiley & Sons, Ltd.

Recent advances in telecommunication technology, including wireless networks and the Internet, along with the competition of network operators for offering advanced and different services, are putting increasing pressure for building telecommunication software systems that are adaptive to new requirements and easily reconfigurable, even in run time. We propose a new modelling primitive - coordination contract - that we have developed and applied to other applications domains, as a means to provide an effective solution to this problem. We briefly describe coordination contracts and discuss how they can support the evolution of the specifications of the Wireless Application Protocol (WAP) Datagram layer.

In this paper, we address dynamic reconfiguration from the point of view of the enforcement of the policies that organisations wish to see imposed through the way information systems support business. We address the process of evolution by proposing a primitive-coordination context-for modelling the circumstances in which reconfiguration can and should take place. The idea is for business policies to emerge as properties of process executions when controlled through the coordination contexts that will have been defined for supporting business activities.

For several different reasons, such as changes in the business or technological environment, the configuration of a system may need to evolve during execution. Support for such evolution can be conceived in terms of a language for specifying the dynamic reconfiguration of systems. In this paper, continuing our work on the development of a formal platform for architectural design, we present a high-level language to describe architectures and for operating changes over a configuration (i.e., an architecture instance), such as adding, removing or substituting components or interconnectons. The language follows an imperative style and builds on a semantic domain established in previous work. Therein, we model architectures through categorical diagrams and dynamic reconfiguration through algebraic graph rewriting.

Software architecture has put forward the concept of connector to express complex relationships between system components, thus facilitating the separation of coordination from computation. This separation is especially important in mobile computing due to the dynamic nature of the interactions among participating processes. We present connector patterns, inspired in Mobile UNITY, that describe three basic kinds of transient interactions: action inhibition, action synchronization, and message passing. The connectors are given in COMMUNITY, a UNITY-like program design language which has a semantics in category theory. We show how the categorical framework can be used for applying the proposed connectors to specific components and how the resulting architecture can be visualized by a diagram showing the components and the connectors.

Summary Since Pnueli’s seminal paper in 1977, Temporal Logic has been used as a formalism for specifying and verifying the correctness of reactive systems. In this paper, we show that, besides its expressive power, Temporal Logic enjoys a very strong structural property: it is categorical on processes. That is, we show how temporal specifications (as theories) can be embedded in categories of process behaviour, and out of this adjunction we build an institution that is categorical in the sense of Meseguer. This characterisation means that temporal logic is, in a sense, ‘sound and complete’ with respect to process specification and interconnection techniques.

The necessity to deal simultaneously with different formalisms seems to be intrinsic to the discipline of Software Engineering, particularly in relation to modularity, reusability and incremental ity. In order to accommodate this diversity of formalisms, some authors have proposed the adoption of a common semantic domain for the different specification languages, and their transla tion into a common style of predicate logic. In this paper, we suggest that an alternative approach may be taken where the different modelling approaches are formalised individually in a common mathematical framework – Category Theory, and relationships are established between them using functors. Several examples are adduced to support this view and the generality of the approach is illustrated by formalising reusability as a property of a functor relating two such formalisms.

Abstract In this paper, we bring together the use of temporal logic for specifying concurrent systems, in the tradition initiated by A. Pnueli, and the use of tools from category theory as a means for structuring specifications as combinations of theories in the style developed by R. Burstall and J. Goguen. As a result, we obtain a framework in which systems of interconnected components can be described by assembling the specifications of their components around a diagram, using theory morphisms to specify how the components interact. This view of temporal theories as specification units naturally brings modularity to the description and analysis of systems. Moreover, it becomes possible to import into the area of formal development of reactive systems the wide body of specification techniques that have been defined for structuring specifications independently of the underlying logic, and that have been applied with great success in the area of Abstract Data Types. Finally, as a discipline of design, we use the object-oriented paradigm according to which components keep private data and interact by sharing actions, with a view towards providing formal tools for the specification of concurrent objects.

Starting from a deontic specification modelling the behaviour of a system, we show how it is possible to reason about the temporal properties of the normative behaviours of that system. In particular, we show how safety and liveness properties can be derived, respectively, from permission and obligation structures. A formal relationship is thus established between the recently proposed deontic accounts of behaviour, that are more action-oriented, and the already traditional and successful property-oriented frameworks based on temporal logics.

The use of modal qualification on terms is advocated for a more intuitive account of the description of the effects of events on objects such as program variables or database attributes, and also for an easier verification of the intended temporal integrity constraints. We develop two logics of modal terms focusing on positional and temporal qualification, and show by means of an example how they can be used to support the description and prescription of actions, as well as to reason about the properties of the specified systems.