ArchLog: Formal approaches for software architectures: component-based and service-oriented computing

« Approches formelles pour les architectures logicielles à base de composants et de services »

The ArchLog group carries out research on formal approaches for component-based and service-oriented architectures. It was created on February 2005 when Prof. Flavio Oquendo moved from the University of Savoie at Annecy to the University of South Brittany at Vannes.

Shortcuts

The Architecture Description Language: π-ADL

The Architecture Analysis Language: π-AAL

The Architecture Refinement Language: π-ARL

Ambient intelligence

Sensor-actuator networks

Mobile agent systems

Human-computer interfaces for monitoring systems

Grid computing systems

Enterprise application integration systems

Software systems targeting J2EE platforms

Overall objectives

Keywords: architecture description languages, architecture analysis languages, architecture refinement languages, formal development techniques, π-calculus, dynamic software architectures, ambient intelligence

One of the most challenging tasks in software engineering is to assure continuous correctness, especially as software systems are increasingly used in highly dynamic and often distributed, mobile and context-aware environments such as in ambient intelligence applications. In order to reach this grand objective, the following open issues need to be addressed:

to support the formal specification of software systems whose architecture can change, on-the-fly, at run-time;
to support their automated analysis with respect to functional as well non-functional properties;
to support their property-preserving transformations and application synthesis, by stepwise refinement from abstract to concrete specifications and full code generation, as well as their subsequent evolution;
to support compliance with respect to application requirements on-the-fly, i.e. if requirements change, enable the software system to safely change to continuously cope with requirements.

In order to address these issues, the ArchLog group defines and develops languages, processes and tools to support the continuous specification, analysis, refinement, and compliant evolution of software systems, in particular ambient intelligence software systems. Indeed, a holistic formal engineering approach is needed that does not concentrate on one-shot software development but rather on continuous engineering and on-the-fly adaptation of software systems. Our work for defining and developing a holistic solution relies on a formal architecture-centric model-driven engineering approach.

Why formal?

Correctness of software systems can be improved by formalising different products and processes in the life-cycle. Among the reasons to apply formal foundations to our languages and tools are: to improve documentation and understanding of specifications, to enable rigorous analysis of the system properties, to be as certain as possible that the transformations and implementation are property-preserving and error-free, to improve rigour and quality of the whole development process, and to provide a firm foundation during the adaptation and evolution process.

Why architecture-centric?

Software architecture has emerged as an important subdiscipline of software engineering. A key aspect of the design of any software system is its architecture, i.e. the fundamental organisation of the system embodied in its components, their relationships to each other, and to the environment, and the principles guiding its design and evolution. Software architecture forms the backbone for building successful software-intensive systems. Architecture descriptions provide thereby the conceptual abstraction for modelling complex software systems during development and then during deployment and on-the-fly adaptation and evolution.

Why model-driven engineering?

All forms of engineering rely on models to design real-world systems. Models are used in many ways: to understand specific system aspects, predict system qualities, reason about impact of changes, and communicate major system features to stakeholders. In a model-driven approach, i.e. the system models have sufficient detail to enable the generation of a full system implementation from the models themselves. Indeed, “the model is the code”, i.e. the focus is on modelling and code is mechanically generated from models. In an architecture-centric model-driven engineering approach, models are component-based architectural (run-time) models. They support model analysis, property-preserving transformations, and application synthesis.

More precisely, our objective is to define and develop an integrated set of formal architecture-centric languages, processes, and tools for the model-driven engineering and continuous evolution of software systems based on the π-calculus and related theories. It comprises: (a) formal architecture description, analysis, and refinement languages for specifying the architecture of evolvable software systems, verifying their properties and expressing their refinements; (b) tools to support architecture description, analysis, and refinement as well as code generation; (c) enactable processes for supporting model-driven engineering and continuous evolution relying on a persistent run-time virtual machine for process enactment.

Scientific foundations

In order to reach the overall objective, the scientific foundations of our work comprise the triad:

theoretical foundations: design and definition of formal languages based on the π-calculus for architecture description, on the μ-calculus for architecture analysis, and on the rewriting logic for architecture refinement;
methodological foundations: design and integration of the formal languages in order to define and transform component-based architecture-centric models in terms of the model-driven engineering paradigm;
technological foundations: design and implementation of the languages using a persistent model repository in order to support model-driven process integration (where process models are described in the languages themselves) and tool integration according to a service-oriented architecture.

Relying on these foundations, we defined:

an architecture description language (called π-ADL) based on the typed higher-order π-calculus in order to support the formal specification of software architecture models that can change, on-the-fly, at run-time;
an architecture analysis language (called π-AAL) based on the μ-calculus in order to support automated model analysis with respect to functional as well non-functional properties;
an architecture refinement language (called π-ARL) based on the rewriting logic in order to support property-preserving transformations and application synthesis, by stepwise refinement from abstract to concrete model specifications and full code generation, as well as their subsequent evolution;
all these languages to enable change at run-time in order to support compliance with respect to application requirements on-the-fly, i.e. if requirements change, enable the software system models and the system itself to safely change to continuously cope with requirements.

Indeed, these integrated languages provide features to formally model, reason about and refine the structure and behaviour of dynamic software systems (in terms of architectural components and connectors) and support their dynamic evolution. The π-ArchWare integrated development environment itself, based on these languages, is constructed as a dynamic software system using a bootstrap approach.

The focus of the ArchLog group is therefore on languages, processes and tools for the formal modelling of dynamic software systems (evolvable at design, build and runtime), and for the computer-aided formal analysis and refinement of these models.

The core language is the π-ADL. It is a strongly typed persistent language that has a formal operational semantics supporting execution by a virtual machine. Thus, it can be used as a specification, prototype or implementation language. Thereby, using π-ArchWare, one can not only model a dynamic software system, analyze and refine it, but actually code it. In fact, one can use π-ADL as a specification language to formally specify the architecture of a complex software system in terms of its components and connectors, then as a high-level prototyping language, in which a prototype of the software system can be quickly developed, analysed and experienced, then refine the prototype in a incremental way to build the end-user system that, once deployed, can evolve using π-ArchWare itself.

The novelty of the π-ArchWare approach lies in its holistic view of software systems. This starts with the capturing of the key architectural decisions by the definition of architecture styles, which might also involve the specification of invariant properties of the software (w.r.t. aspects such as structure, behaviour and qualities). Such properties may then be checked/proved using analysis tools throughout the software life cycle. Since π-ArchWare accommodates both static and dynamic qualities, it is essential that the run-time system can provide feedback and evolve while preserving the defined properties according to any policy and constraint defined at the level of the architectural style.

π-ArchWare goes beyond existing software environments in supporting architecture-centric engineering of software systems. In π-ArchWare both the software engineering process and its products at every stage of the software life cycle, including specification, implementation, qualities and indeed architectural styles themselves, are run-time evolvable. While existing software environments have proposed and implemented mechanisms for particular evolutionary scenarios, ArchWare addresses the problem of architecture-centric evolution at all levels of abstraction throughout the life-cycle of a software system.

The engineering of evolvable software systems requires the capture of key design decisions about “how” the software is to function in terms of expected behaviours, “what” is its structure in terms of components and their connectors, and “which” qualities are to be guaranteed. Furthermore, an appropriate refinement process (describing “how to build” the software) is also to be effectively supported.

A further central aspect of π-ArchWare is the support for the dynamic evolvability of applications and embedded processes. ArchWare enables deployed software architectures to evolve, in a controlled manner, in order to address aspects such as run-time evolution of requirements and technology.

π-ArchWare follows a formal architecture-centric model-driven engineering approach. Models are used in many ways: to understand specific system aspects, predict system qualities, reason about impact of changes, and communicate major system features to stakeholders.

Models are at the heart of the π-ArchWare approach. Definitely, π-ArchWare implements formal model-driven engineering, i.e. the formal models have sufficient detail to enable the generation of a full system implementation from the models themselves. Indeed, “the model is the code”, i.e. the focus is on modelling and code is mechanically generated from models. In π-ArchWare, models are architecture-centric (run-time) models. They are executable and support analysis and refinement. This is illustrated in the figure below which shows a variety of architecture-centric model-driven activities and stakeholders that may be used when developing applications in π-ArchWare.

π-ArchWare architecture-centric model-driven software engineering

Typical architecture-centric activities are “define style”, “define architecture”, and “refine architecture” (the last refinement is code generation). Typical stakeholders are “style architect”, “application architect”, and “application engineer”.

“Define style” activities, whose principal actors are the “style architects”, represent the top level inception of a family of software architectures. An architecture style defines a domain specific architecture description “profile”, including formal definitions of what an architectural element is, and what its invariant properties (including qualities) are, how elements can be combined, which constraints apply, and which processes can be applied to architecture elements and whole architecture descriptions (notably w.r.t. refinement and evolution).

“Define architecture” activities, whose principal actors are the “application architects”, may use the domain specific styles defined by the style architect to describe a specific software architecture. In ArchWare an architecture description conforms to the properties and constraints defined by its style and can represent a system at various levels of abstractions (w.r.t. the detail of implementation decisions provided by the application engineer).

“Refine architecture” activities, whose principal actors are the “application engineer”, support refinement transformations from abstract to more concrete architecture descriptions. Thus, an abstract – platform independent – architecture description can be refined to a concrete – platform specific – description of a specific application. The role of the application engineer is to derive that concrete description by applying correctness preserving refinements that conform to the constraints defined by the application architect and by the adopted architecture styles.

It is worth noting that this software engineering process model is not hard-coded in π-ArchWare. It is one possible architecture-centric software engineering process model that can be explicitly defined and enacted in π-ArchWare. π-ArchWare provides a library of software engineering process models that includes this one and they are all evolvable.

Application domains

Keywords: ambient intelligence, sensor-actuator networks, mobile agent systems, human-computer interfaces for monitoring systems, grid computing systems, enterprise application integration systems, software systems for targeting J2EE platforms, component-based architectures, service-oriented architectures, process-oriented architectures

π-ADL, and its associated languages π-AAL and π-ARL, have been applied in several application domains:

ambient intelligence,
sensor-actuator networks,
mobile agent systems,
human-computer interfaces for monitoring systems,
grid computing systems,
enterprise application integration systems,
software systems targeting J2EE platforms.

All these domains are characterised by the need of architecture description, analysis and refinement languages powerful enough, in terms of expressiveness, to model dynamic architectures, including support for modelling the structure, behaviour and qualities of mobile and context-aware systems.

The different applications of π-ADL, and its associated languages and tools are broad and general enough to demonstrate their adequacy and relevance for addressing innovative industrial problems. Furthermore, the π-ArchWare software environment itself is a validation of π-ADL and associated languages and tools since it has been completely specified and developed using π-ADL itself.

Ambient intelligence

The concept of ambient intelligence provides a wide-ranging vision on how the information society will develop. As a new paradigm for information and communications technologies, we believe that ambient intelligence will open the door to major new application opportunities.

More precisely, ambient intelligence stems from the convergence of three key technologies: ubiquitous computing, ubiquitous communication, and intelligent user friendly interfaces. Ubiquitous computing means integration of microprocessors into everyday objects. Ubiquitous communication enables these objects to communicate with each other and the user by means of possibly wireless, possibly ad-hoc, networks. An intelligent user friendly interface enables the inhabitants of the ambient intelligence environment to control and interact with the environment in a natural and personalised way (e.g. preferences, context). On convergence humans will be surrounded by intelligent interfaces supported by computing and networking technology that need to be properly integrated with business and social structures.

The ambient intelligence landscape is a world in which there are almost uncountable interoperating devices. Most will be wireless, some wired, many will be mobile, and many will be fixed. The networks will thus be configurable on an ad hoc basis according to a specific perhaps short-lived task with variable actors and components. This ubiquitous computing must also be pervasive. These devices will use ‘peer to peer’ mechanisms to communicate with each other, and with the surrounding infrastructure (e.g. a local intranet or Internet). In a mobile ad hoc network, since the nodes are mobile, the network topology may change rapidly and unpredictably over time. The network is thereby decentralized.

π-ArchWare is a holistic response to the design challenge posed by ambient intelligence on the development of systems exploiting ambient intelligence technologies. It is holistic in the sense that it considers the software system and the application that it supports to be a single entity. Thus, this entity is constructed to remain dynamically compliant to the needs of the application as it changes and evolves in the context of an ambient environment. It is not a classical autonomic system in the sense that it is it does not attempt to limit itself to being a completely self-managing environment. Rather it seeks to allow the human user and its context to continually influence and adapt the software system, whilst continuing to guarantee fitness of purpose and the integrity of service of the whole system in terms of safety and liveness properties.

Because continuous compliance is an open-ended commitment in the light of unpredictable requirements and context-aware systems, everything must be designed for dynamic and sustainable change.

π-ADL has been from its inception designed to address the architecture-centric formal development of systems with emergent behaviour, which can be dynamic, open, mobile, context-aware and ubiquitous, being able to evolve on the fly.

In the following we present different applications of π-ADL, and its associated languages and tools, that address different aspects of ambient intelligence environments, in particular sensor-actuator networks and mobile agents.

Sensor-actuator networks

Sensor-actuator networks are comprised of sensor and actuator nodes that communicate among each other using links to perform distributed sensing and actuation tasks. In these applications, sensors are engaged in gathering information about the physical environment, while actuators are involved in taking decisions and then performing appropriate actions in the area of interest. They are part of most ambient intelligence systems.

Intelligent instruments are composed of networks of sensors and actuators that are able to provide complex services such as diagnostic, validation, communication, learning, in order to jointly control a physical system. The design of such intelligent instruments needs multidisciplinary skills, comprising skills in physics, mechanics and computing sciences. Most of the time, the system architect in charge of designing the embedded software for such instruments is a domain expert but not a software engineer. Moreover, strong constraints coming from the hardware are imposed at the software level.

One way of addressing this problem is to define an architecture style that is specific to the design of intelligent instruments, including the specification of all structural and behavioural properties that must be satisfied by architectures that conform to this style, and define transformation models to automatically refine this design to target platforms, including code generation of the full application.

Jérôme Revillard et al. defined and developed this architectural style, refinement models, and application generator. They designed, implemented and applied the customised π-ArchWare model driven environment for sensor-actuator networks to generate software to control a robot with a glove, the 18-sensor CyberGlove. The robot is a Lego Mindstorm, which comprises an autonomous programmable microcomputer, using a Hitachi H8/3932 microcontroller that can be used to control actuators, like a sound generator, lights, and motors, and read input from various sensors, like light sensors, pressure sensors, rotation sensors, and temperature sensors. It has an infrared transceiver for downloading software components and communicating with other robots.

Mobile agent systems

Mobile agents form one of the most promising approaches to face the problems encountered in the decentralised systems, including ambient intelligence systems. However, the use of mobile agents is still unsafe. This is due to the lack of formal methods for modelling and developing mobile agent systems.

Selma Azaiez et al. defined and developed an architectural style, refinement models, and application generator. They designed, implemented and applied the customised π-ArchWare model driven environment for mobile agent systems. The architecture style is based on the Mobile Agent System Interoperability Facility (MASIF) OMG Standard. From the generic architecture, the system architect derives by refinement the concrete architecture, from which the code is generated. The reference architecture is formalized with π-ADL and the refinement models with π-ARL. The software environment was applied to design and generate a decentralised deployment system where mobile agents move to different remote hosts in order to update deployed applications.

Human-computer interfaces for monitoring systems

As in lots of industrial processes, particle accelerators at CERN, the European Organization for Nuclear Research, are composed by a large amount of heterogeneous systems. These heterogeneous systems are monitored using customised Human Computer Interfaces (HCIs), intermediate databases, and numerous sensors.

The CERN’s Technical Control Room has defined a design method used to architect the HCIs of monitoring systems in order to efficiently restart a particle accelerator after a major breakdown. At CERN, this design method is the basis for the development of a family of HCIs for monitoring systems, HCIs that must follow accurate rules in order to be easily understood and efficiently used by the control room operators.

Olivier Ratcliffe et al. defined an architectural style with π-ADL and π-AAL in order to formalise all the rules defined at that method and used them to construct a domain-specific software development environment for designing and generating monitoring software systems, including their HCIs. This software environment, based on π-ArchWare, called SEAM (Software for the Engineering of Accelerator Monitoring), guides the design of the HCIs and generates the code of particle accelerator monitoring software systems. SEAM has numerous benefits, such as the ability to reuse efficiently previous design experience and the possibility to use architectural tools to perform analyses on the HCI architectures. It supports the generation of monitoring applications that comply at best with the user requirements and can evolve whenever user requirements evolve, thereby exploiting π-ArchWare features for supporting compliant evolution.

Grid computing systems

The Grid paradigm is described as a distributed computing infrastructure for advanced science and engineering that can address the concept of coordinated resource sharing and problem solving in dynamic, multi-institutional virtual organizations. This coordinated sharing can provide direct access to computers, software, files, data and other system resources. Grid applications bundle different services using a heterogeneous pool of resources in virtual organization. This makes Grid applications very difficult to model and to implement.

It is a commonly recognized statement that Grid applications have seldom been designed using formal techniques although from past experience such techniques have shown advantages.

π-ADL, and associated languages and tools, are the base of a formal engineering approach to Grid application development. It addresses quality of service and cross platform developments by applying the model-driven engineering paradigm to formal architecture-centric engineering. This combination benefits from the formal modelling of the Grid application in addition to model-based transformations. It significantly eases application development in Grid computing.

David Manset et al. defined and developed a novel architectural style, refinement models, and application generator. They designed, implemented and applied the customised π-ArchWare model driven environment for Grid computing systems. Applying π-ARL, they address the challenge of designing, optimizing and adapting Grid-abstract architectures, with respect to different criteria, in order to automatically refine and generate a complete set of Grid services to be deployed on a physical grid of resources. The implemented software environment has been applied to the development of the MammoGrid application, which aims to develop a European-wide database of mammograms used to support effective co-working between healthcare professionals throughout the European Union.

Enterprise application integration systems

Industry is increasingly seeking effective ways of accessing larger geographically distributed information coming from heterogeneous applications in order to control its production system. The emergence of Enterprise Application Integration (EAI) middleware is a step in this direction, but it is only part of the solution. Several issues remain to be solved w.r.t. integration of heterogeneous enterprise applications in a global and consistent solution. This requires extensive support in order to model, generate, and evolve on-the-fly the EAI-based integrated systems.

Thésame and Agilium have developed an EAI middleware which can be used to track processes and products for a variety of purposes. Its modelling notation can describe different applications by taking into account product and process descriptions, relationships between activities, and execution traceability (product transformation by a process activity). This EAI middleware is suitable to large-scale production management systems cutting across different organisations.

The ArchWare European project has set up pilot projects to validate in a real set π-ADL, and its associated languages and tools. The pilot project at Thésame/Agilium aimed to architect, refine, generate, and evolve on-the-fly agile integrated industrial process systems based on EAI middleware.

Régis Dindeleux et al. defined and developed a novel architectural style, refinement models, and application generator. They designed, implemented and applied the customised π-ArchWare model driven environment for agile integrated industrial process systems based on their EAI middleware. Using that software environment, they were able to develop a family of agile integrated industrial process systems for SME-SMIs.

Software systems targeting J2EE platforms

As cited above, the ArchWare European project has set up pilot projects to validate in a real set π-ADL, and its associated languages and tools. The pilot project at Engineering Ingegneria Informatica aimed to architect, refine, generate, and evolve software systems whose the target programming language is Java and the target platform J2EE.

Carmela Occhipinti et al. defined and developed architectural styles, refinement models, and an application generator for Java/J2EE. They designed, implemented and applied the customised π-ArchWare model driven environment for software systems targeting J2EE platforms. Using that software environment, they were able to develop a federated knowledge management system fully generated in Java/J2EE.

In addition, work has just started for developing a π-MDE for distributed simulation software based on the High Level Architecture, a general purpose architecture for simulation reuse and interoperability.

Software Tools

Keywords: architecture description tool, architecture animation tool, architecture analysis tool, architecture refinement tool, UML profile for architecture description, code generation, virtual machine, integrated development environment

A major impetus behind developing formal languages for architecture description is that their formality renders them suitable to be manipulated by software tools. The usefulness of an architecture description language is thereby directly related to the kinds of tools it provides to support architectural description, but also animation, analysis, refinement, code generation, and evolution. Indeed, π-ADL, and its associated languages π-AAL and π-ARL, are supported by a comprehensive toolset for supporting architecture-centric formal development. It is composed of:

π-Modeller: a tool to support visual description of software architectures in π-ADL – it is implemented using GME – Generic Modelling Environment;
π-Animator: a tool to support graphical animation of software architectures described in π-ADL – it is implemented using Java and XSB Prolog;
π-Analyser: a tool to support verification of structural and behavioural properties specified in π-AAL against software architectures described in π-ADL – it is implemented using MMC – Mobility Model Checker – and XSB Prolog;
π-Refiner: a tool to support refinements of software architectures described in π-ADL where these refinements are modelled and automated in π-ARL – it is implemented using the Maude rewriting logic system;
π-UML Modeller: a tool to support visual description of software architectures in UML (using the UML profile for π-ADL) – it is implemented as an extension of the Objecteering UML Modeller;
π-Synthesiser: a tool to support code generation from concrete architecture descriptions in π-ADL – a π-ADL-to-Java code generator tool has been synthesized – it is implemented in PBase;
π-ADL Compiler and Virtual Machine: a π-ADL callable compiler and persistent virtual machine, implemented in the PBase persistent language;
π-TraceChecker: an online model checking tool based on CADP – it checks if traces produced by the π-ADL virtual machine satisfy properties specified in π-AAL;
π-Browser: a process-oriented browser for managing architecture descriptions created in the persistent store of the π-ADL virtual machine – implemented in π-ADL itself.

The first four tools have been designed and developed in our group. The fifth has been designed in our group and developed by CPR/Engineering (Italy). The sixth and seventh developed at the University of Saint Andrews (UK) and the last two at INRIA Rhône-Alpes and University of Manchester (UK), respectively.

All these tools are available as open source software at http://www.architecture-ware.org as part of the ArchWare OSS (Open Source Software) release.

Besides these tools, we have developed domain-specific integrated development environments based on π-ADL and the Model-Driven Engineering approach (the so-called π-ArchWare MDE environments). They are implemented by customisation of π-ADL, and its associated languages π-AAL and π-ARL, and tools. Indeed, the languages and tools were designed to support customisation and evolution.

As presented so far, the following model-driven engineering environments supporting the architecture-centric formal development of software systems were developed:

π-ArchWare MDE for sensor-actuator networks,
π-ArchWare MDE for mobile agent systems,
π-ArchWare MDE for human-computer interfaces for monitoring systems,
π-ArchWare MDE for grid computing systems,
π-ArchWare MDE for enterprise application integration systems,
π-ArchWare MDE for software systems targeting J2EE platforms.

These π-ArchWare MDE software environments pave the way to formally develop software systems for ambient intelligence environments.

Besides providing languages, processes, and tools for formal architecture-centric model-driven engineering, the π-ArchWare software environments enforce a novel relationship between software systems and their development environments. Indeed, in the π-ArchWare approach, software systems and the software development environments that support their engineering are both evolving artefacts; the keystone of π-ArchWare is recognising that compositional, architecture-centric evolutionary approaches (supported by adequate formal languages, processes, and tools) are needed to effectively construct and operate both kinds of systems. Thus, π-ArchWare solutions are applied consistently to the software systems being engineered as well as to the software engineering process and environment themselves. Jointly, they exploit the many advantages of the π-ArchWare architecture-centric compositional and evolutionary framework. This gives the possibility of an ongoing link between software systems and their software engineering processes in order to support continuous evolution, thereby accommodating change over their lifetime.

Research results

Keywords:π-ADL (architecture description language), π-AAL (architecture analysis language), π-ARL (architecture refinement language), π-calculus

The ArchLog group applies an innovative approach to the formal architecture-centric model-driven engineering of software systems that sets the “ability to change by composition/de-composition/re-composition” as its central characteristic. According to this approach, since 2002 and in particular in 2004 and 2005, the work of the ArchLog group has been focused on the development of the languages, processes and tools, as part of the π-ArchWare formal architecture-centric model-driven engineering environment. In particular, the ArchLog group designed novel languages for describing dynamic architectures, analysing architecture structural and behavioural properties, and refining architecture descriptions:

π-ADL: an architecture description language based on the π-calculus in order to support the formal specification of software architecture models that can change, on-the-fly, at run-time;
π-AAL: an architecture analysis language based on the μ-calculus in order to support automated model analysis with respect to functional as well non-functional properties;
π-ARL: an architecture refinement language based on the rewriting logic in order to support property-preserving transformations and application synthesis, by stepwise refinement from abstract to concrete model specifications and full code generation, as well as their subsequent evolution.

The validation of π-ArchWare languages, processes and tools are carried out through realistic case studies and industrial pilot projects. Its dissemination is done as Open Source Software.

The Architecture Description Language: π-ADL

In our work, architecture description encompasses two aspects: the expression and verification of architectural styles (typically carried out by style architects) and of software architectures themselves (typically carried out by application architects).

The π-ADL provides the core structure and behaviour constructs for describing dynamic software architectures. It is a formal specification language designed to be executable and to support automated analysis and refinement of dynamic architectures.

The π-ADL has as formal foundation the higher-order typed π-calculus [76], a higher-order calculus for communicating and mobile systems. The π-ADL is itself a formal language defined as a domain-specific extension of the higher-order typed π-calculus: it is a well-formed extension for defining a calculus of communicating and mobile architectural elements.

The π-ADL takes its roots in previous work concerning the use of π-calculus as semantic foundation for architecture description languages [44][43]. Indeed, a natural candidate for expressing dynamic (run-time) behaviour would be the π-calculus as it is [68], which provides a general model of computation and is Turing-complete. This means that in π-calculus “every computation is possible but not necessarily easy to express”. In fact, the classical π-calculus is not suitable as an architecture description language since it does not provide architecture-centric constructs to easily express architectures in particular w.r.t. architectural structures. Therefore, a language encompassing both structural and behavioural architecture-centric constructs is needed. The π-ADL is this encompassing language, defined as a domain-specific extension of the higher-order typed π-calculus. It achieves Turing completeness and high architecture expressiveness with a simple formal notation.

The following general principles guided the design of π-ADL:

formality: π-ADL is a formal language: it provides a formal system, at the mathematical sense, for describing dynamic software architectures and reasoning about them;
π-ADL focuses on the formal description of software architectures from the run-time viewpoint: the (run-time) structure, the (run-time) behaviour, and how these may evolve over time;
executability: π-ADL is an executable language: a virtual machine runs specifications of software architectures;
user-friendliness: π-ADL supports different concrete syntaxes – textual and graphical (including UML-based) notations – to ease its use by architects and engineers.

Based on these general principles, the design of π-ADL followed the following language design principles [72][79][80]:

the principle of correspondence: the use of names are consistent within π-ADL, in particular there is a one to one correspondence between the method of introducing names in declarations and parameter lists;
the principle of abstraction: all major syntactic categories have abstractions defined over them (in π-ADL, it includes abstractions over behaviours and abstractions over data),
the principle of data type completeness: all data types are first-class without any restriction on their use.

In first-class citizenship, i.e. in addition to rights derived from type completeness (i.e. where a type may be used in a constructor, any type is legal without exception), there are properties possessed by all values of all types that constitute their civil rights in the language. In π-ADL they are:

the right to be declared,
the right to be assigned,
the right to have equality defined over them,
the right to persist.

Additionally, π-ADL provides an extension mechanism, i.e. new constructs can be defined on top of the language using user-defined mixfix abstractions. This extension mechanism provides the basis for providing style-based definitions.

In π-ArchWare, a style notation, built on the π-ADL, provides the style constructs from which the base component-and-connector style and other derived styles can be defined. Conceptually, an architectural style includes:

a set of abstractions for architectural elements,
a set of constraints (i.e. properties that must be satisfied) on architectural elements, including legal compositions,
a set of additional analyses that can be performed on architecture descriptions constructed in the style.

π-ArchWare provides a novel ADL that is general-purpose and Turing-complete. The advantage w.r.t. other ADLs is that the π-ADL supports user-defined architectural component-and-connector abstractions (instead of being obliged to use hard-coded abstractions provided by particular ADLs that very often do not meet architect needs). It can be seen as a second generation ADL: in first generation ADLs, languages were not complete and architectural (run-time) concepts were hard-coded as language constructs; in second generation, languages should be complete and architectural (run-time) concepts should be customisable.

The Architecture Analysis Language: π-AAL

In π-ArchWare, architecture analysis encompasses two aspects: the expression and verification of properties of architectural styles (typically carried out by style architects) and of software architectures themselves (typically carried out by application architects).

The π-AAL provides a uniform framework for specifying relevant properties of styles and architectures. These properties have different natures: they can be structural (e.g. cardinality of architectural elements, interconnection topology) or behavioural (e.g. safety, liveness, and fairness defined on actions of the system). The π-AAL complements the π-ADL with features allowing architects to express and verify properties of software architectures and styles in a natural way. Analysis is intended to be performed according to three approaches: model-checking, theorem proving and specific external tools.

The π-AAL is a formal property expression language designed to support automated verification. Thereby, one can mechanically check whether an architecture described in π-ADL satisfies a property expressed in π-AAL.

The π-AAL has as formal foundation the modal μ-calculus [60], a calculus for expressing properties of labelled transition systems by using least and greatest fixed point operators. π-AAL is itself a formal language defined as an extension of the μ-calculus: it is a well-formed extension for defining a calculus for expressing structural and behavioural properties of communicating and mobile architectural elements.

The π-AAL takes its roots in previous work concerning the extension of modal operators with data-handling constructs [66], the use of regular expressions as specification formalism for value-passing process algebras [49], and the extension of fixed point operators with typed parameters [55].

Indeed, a natural candidate for “pure” behavioural properties would be the modal μ-calculus, which is a very expressive fixed point-based formalism subsuming virtually all temporal logics defined so far in the literature [77]. However, since π-AAL must also provide features for expressing structural properties of architectures, the modal μ-calculus is not sufficient. Therefore, a formalism encompassing both the predicate calculus and the modal μ-calculus is needed. The π-AAL is, thereby, this encompassing formalism, defined as a domain-specific extension of the μ-calculus.

The π-AAL combines predicate logic with temporal logic in order to allow the specification of both structural and behavioural properties. It enables automated verification of property satisfaction by model checking (through on-the-fly model checking) or theorem proving (through deductive verification using tabled logic programming).

The Architecture Refinement Language: π-ARL

Software applications are usually developed in several steps. Indeed, the concrete architecture of a software system is often developed through vertical and horizontal refinements of related architectures that differ respectively w.r.t. abstraction and partition dimensions.

Vertical refinement steps add more and more details to abstract models until the concrete architectural model is described. A vertical refinement step typically leads to a more detailed architecture description that increases the determinism while implying properties of the abstract description. Generally, an abstract architecture is smaller and easier to understand and a concrete architecture reflects more implementation concerns.

Horizontal refinement is concerned with partitioning of an architecture. For instance, partitioning an abstract component in its parts at the same abstraction level.

π-ArchWare supports both vertical and horizontal refinement. In π-ArchWare, the underlying approach for architectural refinement is underspecification, i.e. at a high-level of abstraction, when specifying an architectural element, certain aspects can be left open. The decrease of this underspecification establishes a refinement relation for architectural elements.

A refinement relation in π-ArchWare, from an external or internal point of view, comprises four forms of refinement:

behaviour refinement,
port refinement,
structure refinement,
data refinement.

In behaviour refinement, the underspecification may concern the external (observable) behaviour or the internal behaviour of an architectural element. The external behaviour of an architectural element is the behaviour that its environment can observe, i.e. its behaviour from an external point of view. The internal behaviour concerns the internal expression of behaviour within the scope of the architectural element. The structure of an architectural element is its internal structure in terms of sub-architectural elements and their connected ports, i.e. the structure within the scope of the architectural element from an internal point of view. The ports of an architectural element provide the interaction points (i.e. connections) between the element and its environment, i.e. its ports from an external point of view.

The most fundamental notion of refinement in π-ArchWare is behaviour refinement. The other forms of refinement imply behaviour refinement modulo port, structure and data mappings.

In general, architectural refinement is a combination of the four forms of refinement. For instance, an architect can define an abstract architecture, then “data” refine that architecture in order to introduce base and constructed data types, then “port” refine the architecture to have ports with finer grain connections carrying data of different types, then “structure” refine its composite behaviour by adding new finer grain connectors, and so on.

The π-ARL provides constructs for defining refinements of the four forms cited so far, according to external or internal points of view. Composite refinements can be defined in terms of refinement primitives and composite refinements themselves. Refinement primitives comprise:

adding, removing, replacing or transforming data type declarations of an architecture,
adding, removing, replacing or transforming ports of an architecture,
adding, removing, replacing or transforming output and input connections of ports of an architecture,
transforming the behaviour of an architecture or the behaviour of a component or connector in an architecture,
adding, removing, replacing or transforming components or connectors in an architecture,
exploding or imploding components or connectors in an architecture,
unifying or separating connections of ports in an architecture.

These primitives, applied step by step, allow the incremental transformation of an architecture description. These transformations are enforced to be refinements if preconditions of refinement primitives are satisfied and proof obligations discarded. A refinement engine based on rewriting logic [65][41] runs the refinement descriptions expressed in π-ARL generating further refined architectures. Code is generated from refined (concrete) architectures.

The π-ARL is a formal (executable) refinement language providing architecture-centric refinement primitives and supporting refinement compositions in both vertical and horizontal dimensions, from external or internal points of view. When applied, they refine architectural models described in π-ADL outputting new refined architectural models also in π-ADL.

π-ARL provides the required key features for supporting architecture-centric model-driven formal development. By addressing software development as a set of architecture-centric model refinements, the refinements between models become first class elements of the software engineering process. This is significant because a great deal of work takes places in defining these refinements, often requiring specialized knowledge on source and target abstraction levels, for instance knowledge on the source application logics and on the targeted implementation platforms. Efficiency and quality of software systems can be improved by capturing these refinements explicitly and reusing them consistently across developments. Thereby, user-defined refinement steps can be consistently defined, applied, validated, and mechanically automated.

Related work

Several architecture description languages (ADLs) have been proposed in the literature, including: ACME/Dynamic-ACME [52][53], AESOP [51], AML [81], ARMANI [69], CHAM-ADL [57][58], DARWIN [64], META-H [40], PADL [38], RAPIDE [74][63], SADL [70][71], σπ-SPACE [44][61], UNICON-2 [46], and WRIGHT/Dynamic-WRIGHT [36][37].

ADLs provide both a concrete syntax and a formal, or semi-formal, semantics. Typically, they embody a conceptual framework reflecting characteristics of the domain for which the ADL is intended and/or an architectural style [67].

The focus of π-ArchWare is on languages and tools for the formal modelling of dynamic software architectures (evolvable at design and run-time), and for the computer-aided formal analysis and refinement of these models. In a broad sense the <π-ADL is composed of a set of integrated notations: the architecture description notation (the core), the style definition notation, the property expression notation, and the refinement definition notation. No other ADL provides a comprehensive set of notations for describing dynamic architectures.

But how does π-ArchWare compare with related work? Comparing ADLs objectively is a difficult task because their focuses are quite different. Most ADLs essentially provide a component-and-connector built-in model of architecture description and formalise topological constraints. The reason for this is probably that structure is certainly the most understandable and visible part of an architecture. But behavioural and quality aspects are not completely neglected. They are often taken into account (even if partially) in most ADLs. They are certainly an essential part of architecture description.

π-ADL is the most general among studied ADLs. Instead of hard coding a specific component-and-connector viewpoint model, it is a general-purpose ADL that can be used to define, in a compliant way, different user-defined component-and-connector viewpoint models.

π-AAL provides the notation to express properties of architectures described in π-ADL.

π-AAL combines predicate logic with temporal logic in order to allow the specification of both structural properties and behavioural properties concerning architecture descriptions obtained by instantiating a given style.

Regarding behavioural properties, the choice of modal μ-calculus as the underlying formalism provides a significant expressive power. Moreover, the extension of μ-calculus modalities with higher level constructs such as regular formulas inspired from early dynamic logics like PDL [48] facilitates the specification task of the practitioners, by allowing a more natural and concise description of properties involving complex sequences of actions. The extension of fixed point operators with data parameters also provides a significant increase of the practical expressive power, and is naturally adapted for specifying behavioural properties of value-passing languages such as the π-ADL.

In the context of software architectures, several attempts at using classical process algebras and generic model-checking technology have been reported in the literature. In [56], various architectural styles (e.g., repository, pipe-and-filter, and event-action) are described in LOTOS, by using specific communication patterns and constraints on the form of components, and verified using the CADP toolbox [47][50]. In [75], several variants of the pipe-and-filter style are described in LOTOS and analysed using CADP. In [59], the transformation of software architectures specified in LOTOS and their verification using the XTL model-checker [66] of CADP are presented. Finally, an approach for checking deadlock freedom of software architectures described using a variant of CCS is described in [39]. All these works provide rather ad-hoc solutions for a class of software architectures limited to static communication between architectural elements, and can be subsumed by the more general framework provided by π-ADL/π-AAL and verification tools.

Regarding structural analysis, ACME, ARMANI, CHAM-ADL, DARWIN, RAPIDE, SADL, WRIGHT and others addressed mainly properties like completeness and consistency of software architectures. Most of those approaches propose a less or more sophisticated language for describing properties to analyse.

The main limitation of most of these approaches with regard to π-ArchWare objectives is that they address either structural or behavioural properties, but not both as in π-ArchWare.

As regards architecture refinement, with the exception of a variant of FOCUS [78], i.e. FOCUS/DFA [73], RAPIDE and SADL, there is no proposal for a rigorous calculus based on architectural terms. In the case of SADL the refinement is only structural. In the case of RAPIDE it is only behavioural (supported by simulations). In both cases, clear architectural primitives for refining architectures are not provided and the refinement supported is only partial. π-ARL, like the B [35] and Z [45] formal methods, provides operations to transform specifications. However, unlike FOCUS, B and Z, π-ARL has been specially designed to deal with architectural elements of any architectural style. Unlike SADL, π-ARL supports underspecification. In FOCUS/DFA, refinement is essentially logical implication. In SADL, it is restricted by faithful interpretation. In RAPIDE, it is defined by simulations. In π-ArchWare, it is based on property implication, where the properties to be preserved are defined by the architect.

The π-ARL provides a novel language that on the one side has been specifically designed for architectural refinement taking into account refinement of behaviour, port, structure, and data from an architectural perspective and on the other side is based on preservation of properties. The core of π-ARL is a set of architecture transformation primitives that support refinement of architecture descriptions. Transformations are refinements when they preserve properties of the more abstract architecture. Core properties are built-in. Style-specific or architecture-specific properties are user defined. The underlying foundation for architected behaviours is the higher-order typed π-calculus. Satisfying proof obligations in π-ARL is supported by the π-ArchWare analysis tools, which comprises a model checker, a prover and specific evaluators.

A detailed positioning of π-ADL, π-AAL and π-ARL w.r.t. the state-of-art is given in [62].

International contracts and grants

ArchWare European Project:

Title: Architecting Evolvable Software
Period: January 2002 – June 2005
Funding:European Commission under contract No. IST-2001-32360 in the IST-V Framework Programme
Type: Research
URL: http://www.arch-ware.org/
Role: Scientific direction (Prof. Flavio Oquendo, jointly with Prof. Brian Warboys from the University of Manchester), workpackage leadership (Flavio Oquendo) of workpackages WP1 on the definition of the architecture description language and WP6 on the definition of the architecture refinement language, and key participation in workpackages WP2 on the implementation of the architecture description supporting tools and WP3 on the definition and implementation of the architecture analysis language and supporting tools
Other partners: CPR – Consorzio Pisa Ricerche – Italy, Engineering Ingegneria Informatica – Italy, INRIA – Institut National de Recherche en Informatique et Automatique – France, Thésame – Mécatronique et Management – France, University of Manchester – UK, University of St. Andrews – UK

Staff European Project:

Title: STAFF in Computer Science (Selection, Training and Assessment of Future Faculty)
Period: March 2004 – March 2007
Funding: European Commission under contract No. HRD-271003 in the Asia-Link Programme
Type: Research Training
URL: http://asialink.niit.edu.pk
Role: Partner manager (Prof. Flavio Oquendo), with participation of Prof. Pierre-François Marteau (Aprim) and Prof. Dominique Duhaut (Rimh)
Other partners: University of the West of England, Bristol – UK, Beijing Institute of Technology, Beijing – China, National University of Sciences & Technology, Institute of Information Technology, Rawalpindi – Pakistan

Publications of ArchLog group in 2004-2005

Books and monographs

[1] Oquendo F., Warboys B., Morrison R. (Eds.), Software Architecture, Springer-Verlag, 279 p., May 2004.

[2] Oquendo F., Morrison R. (Eds.), Software Architecture, Springer-Verlag, 262 p., June 2005.

Doctoral dissertation and “Habilitation” theses

[3] Thomas Bolusset, β-Space : Raffinement d’architectures logicielles en amont de la méthode formelle B, PhD thesis, University de Savoie, 320 p., 30 September 2004.

[4] Fabien Leymonerie, ASL : un langage et des outils pour les styles architecturaux – contribution à la description d'architectures dynamiques, PhD thesis, University de Savoie, 249 p., 15 December 2004.

[5] Olivier Ratcliffe, Approche et environnement fondés sur les styles architecturaux pour le développement de logiciels propres à des domaines spécifiques – application au domaine de la supervision du redémarrage d’accélérateurs de particule, PhD thesis, University de Savoie, 227 p., 16 December 2004.

[6] Karim Megzari, Refiner : Environnement logiciel pour le raffinement d’architectures logicielles fondé sur une logique de réécriture, PhD thesis, University de Savoie, 177 p., 17 December 2004.

[7] Jérôme Revillard, Approche centrée architecture pour la conception logicielle des instruments intelligents, PhD thesis, University de Savoie, 246 p., 15 December 2005.

Articles in referred journals and book chapters

[8] Oquendo F., "π-ADL: An Architecture Description Language based on the Higher Order Typed π-Calculus for Specifying Dynamic and Mobile Software Architectures", ACM Software Engineering Notes, Vol. 29, No. 3, pp. 15-28, May 2004.

[9] Arbaoui S., Oquendo F., "Accorder besoins et architectures : un panorama critique", Revue Génie Logiciel, No. 69, pp. 13-20, June 2004 (In French).

[10] Oquendo F., "π-ARL: An Architecture Refinement Language for Formally Modelling the Stepwise Refinement of Software Architectures", ACM Software Engineering Notes, Vol. 29, No. 5, pp. 40-59, September 2004.

[11] Oquendo F., "Formally Refining Software Architectures with π-ARL: A Case Study", ACM Software Engineering Notes, Vol. 29, No. 5, pp. 79-104, September 2004.

[12] Derniame J-C., Oquendo F., "Key Issues and Future Directions in Software Process Technology", European Journal: CEPIS Upgrade, Special Issue on Software Process Technologies, Vol. V, No. 5, pp. 11-16, October 2004 (also printed in the Novática Journal, No. 171, pp. 9-13, September-October 2004).

[13] Oquendo F., "Formally Describing Dynamic Software Architectures with π-ADL", World Scientific and Engineering Transactions on Systems, Vol. 3, No. 8, pp. 673-679, October 2004.

[14] Oquendo F., "Architecture-Centric Model-Driven Development with π-ARL", World Scientific and Engineering Transactions on Computers, Vol. 4, No. 6, pp. 511-520, June 2005.

[15] Oquendo F., "Les architectures logicielles", Encyclopédie de l’informatique et des systèmes d’information, Editions Vuibert (In French) (To appear in 2006).

[16] Oquendo F., "Formally Modelling Software Architectures with the UML 2.0 Profile for π-ADL", ACM Software Engineering Notes (To appear in Vol. 31, No. 1, January 2006).

Publications in international conferences and workshops

[17] Alloui I., Oquendo F., "Describing Software-intensive Process Architectures using a UML-based ADL", Proceedings of the Sixth International Conference on Enterprise Information Systems (ICEIS’04), pp. 201-208, Porto, Portugal, April 2004.

[18] Leymonerie F., Blanc-Dit-Jolicoeur L., Cimpan S., Braesch C., Oquendo F., "Towards a Business Process Formalisation based on an Architecture-centred Approach", Proceedings of the Sixth International Conference on Enterprise Information Systems (ICEIS’04), pp. 513-518, Porto, Portugal, April 2004.

[19] Ratcliffe O., Cimpan S., Oquendo F., Scibile L., "Formalization of an HCI Style for Accelerator Restart Monitoring", Proceedings of the First European Workshop on Software Architecture (EWSA’04), pp. 167-181, St Andrews, UK, Lecture Notes in Computer Science, Springer Verlag, May 2004.

[20] Oquendo F., Warboys B., Morrison R., Dindeleux R., Gallo F., Garavel H., Occhipinti C., "ArchWare: Architecting Evolvable Software", Proceedings of the First European Workshop on Software Architecture (EWSA’04), European Projects in Software Architecture – Invited Paper, pp. 257-271, St Andrews, UK, Lecture Notes in Computer Science, Springer Verlag, May 2004.

[21] Azaiez S., Oquendo F., "GAMA: Towards Architecture-centric Software Engineering of Mobile Agent Systems", Proceedings of the Third International Workshop on Software Engineering for Large-Scale Multi-Agent Systems (SELMAS 2004) at the IEEE/ACM International Conference on Software Engineering (ICSE 2004), pp. 11-20, Edinburgh, UK, May 2004.

[22] Morrison R., Graham K., Balasubramaniam D., Mickan K., Oquendo F., Cimpan S., Warboys B., Snowdon B., Greenwood M., "Support for Evolving Software Architectures in the ArchWare ADL", Proceedings of the Fourth Working IEEE/IFIP International Conference on Software Architecture (WICSA’04), pp. 69-78, Oslo, Norway, June 2004.

[23] Oquendo F., "Formally Describing Dynamic Software Architectures with π-ADL", Proceedings of the Third International Conference on Applied Mathematics and Computer Science (AMCOS’04), pp. 154-160, Rio de Janeiro, Brazil, October 2004.

[24] Azaiez S., Pourraz F., Verjus H., Oquendo F., "Validation by Animation: Animating Software Architectures based on the π-Calculus", Proceedings of the Third Workshop on System Testing and Validation (SV'04), pp. 93-103, Paris, France, December 2004.

[25] Ratcliffe O., Scibile L., Cimpan S., Oquendo F., "Towards an Inductive Definition and Evolution of Architectural Styles", Proceedings of the Seventeenth International Conference on Software and Systems Engineering and their Applications (ICSSEA’04), pp. 31-42, Paris, France, December 2004.

[26] Oquendo F., "Model-Driven Refinement of Software Architectures with π-ARL", Proceedings of the Fourth International Conference on Applied Mathematics and Computer Science (AMCOS’05), pp. 146-152, Rio de Janeiro, Brazil, April 2005.

[27] Cimpan S., Leymonerie F., Oquendo F., "Handling Dynamic Behaviour in Software Architectures", Proceedings of the Second European Workshop on Software Architectures (EWSA’2005), pp. 77-93, Pisa, Italy, Lecture Notes in Computer Science, Springer Verlag, June 2005.

[28] Revillard J., Benoit E., Cimpan S., Oquendo F., "Architecture-Centric Development for Intelligent Instrument Design", IEEE International Conference on Computational Intelligence for Measurement Systems and Applications (CIMSA 2005), pp. 51-62, Giardini Naxos, Italy, July 2005.

[29] Revillard J., Benoit E., Cimpan S., Oquendo F., "Intelligent Instrument Design with ArchWare ADL", Proceedings of the Fifth Working IEEE/IFIP International Conference on Software Architecture (WICSA’05), Working Session Track, Pittsburgh, USA, November 2005 (Proceedings in Press, IEEE Computer Society).

[30] Ratcliffe O., Cimpan S., Oquendo F., "Case Study on Architecture-Centered Design for Monitoring Views at CERN", Proceedings of the Fifth Working IEEE/IFIP International Conference on Software Architecture (WICSA’05), Working Session Track, Pittsburgh, USA, November 2005 (Proceedings in Press, IEEE Computer Society).

[31] Manset D., McClatchey R., Oquendo F., Verjus H., “A Model-Driven Approach for Grid Services Engineering”, Proceedings of the Eighteenth International Conference on Software and Systems Engineering and their Applications (ICSSEA’05), pp. 51-58, Paris, France, November-December 2005.

Internal reports

[32] Nassima Benaissa, Architecture générique et outil logiciel pour les systèmes à agents mobiles, MSc. dissertation, University de Savoie, 82 p., June 2004 (In French).

Miscellaneous<

[33] Oquendo F.: UML 2.0 Profile for the ArchWare Architecture Description Language. Deliverable D1.8, ArchWare European RTD Project, IST-2001-32360, 67 p., June 2005.

[34] Oquendo F.: Tutorial of the ArchWare Architecture Description Language. Deliverable D1.9, ArchWare European RTD Project, IST-2001-32360, 71 p., June 2005.

Bibliography in notes

[35] Abrial J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.

[36] Allen R.: A Formal Approach to Software Architectures. PhD Thesis, Carnegie Mellon University, 1997.

[37] Allen R., Douence R., Garlan D.: Specifying and Analyzing Dynamic Software Architectures. In Fundamental Approaches to Software Engineering, LNCS 1382, Springer Verlag, 1998.

[38] Bernardo M., Ciancarini P., Donatiello L.: Architecting Systems with Process Algebras. Technical Report UBLCS-2001-7, July 2001.

[39] Bernardo M., Ciancarini P., Donatiello L.: Detecting Architectural Mismatches in Process Algebraic Descriptions of Software Systems, Proceedings of the 2nd Working IEEE/IFIP Conference on Software Architecture, Amsterdam, IEEE-CS Press, August 2001.

[40] Binns P., Engelhart M., Jackson M., Vestal S.: Domain-Specific Software Architectures for Guidance, Navigation, and Control. International Journal of Software Engineering and Knowledge Engineering. 1996.

[41] Bolusset T., Oquendo F.: Formal Refinement of Software Architectures Based on Rewriting Logic, ZB2002 International Workshop on Refinement of Critical Systems: Methods, Tools and Experience, Grenoble, Janvier 2002.

[42] Brown A.W.: An Introduction to Model Driven Architecture – Part I: MDA and Today’s Systems. The Rational Edge, February 2004.

[43] Chaudet C., Greenwood M., Oquendo F., Warboys B.: Architecture-Driven Software Engineering: Specifying, Generating, and Evolving Component-Based Software Systems. IEE Journal: Software Engineering, Vol. 147, No. 6, UK, December 2000.

[44] Chaudet C., Oquendo F.: A Formal Architecture Description Language Based on Process Algebra for Evolving Software Systems. Proceedings of the 15th IEEE International Conference on Automated Software Engineering (ASE’00). IEEE Computer Society, Grenoble, September 2000.

[45] Davies J., Woodcock J.: Using Z: Specification, Refinement and Proof. Prentice Hall International Series in Computer Science, 1996.

[46] DeLine R.: Toward User-Defined Element Types and Architectural Styles. Proceedings of the 2nd International Software Architecture Workshop, San Francisco, 1996.

[47] Fernandez J-C., Garavel H., Kerbrat A., Mateescu R., Mounier L., Sighireanu M.: CADP (CAESAR/ALDEBARAN Development Package) – A Protocol Validation and Verification Toolbox, Proceedings of the 8th International Conference on Computer-Aided Verification, New Brunswick, USA, LNCS 1102, Springer Verlag, August 1996.

[48] Fischer M.J., Ladner R.E.: Propositional Dynamic Logic of Regular Programs. Journal of Computer and System Sciences Vol. 18, 1979.

[49] Garavel H.: Compilation et Vérification de Programmes LOTOS. Thèse de Doctorat, Univ. Joseph Fourier (Grenoble), November 1989. Chapter 9: Vérification (In French).

[50] Garavel H., Lang F., Mateescu R.: An Overview of CADP 2001. European Association for Software Science and Technology (EASST) Newsletter, Vol. 4, August 2002.

[51] Garlan D., Allen R., Ockerbloom J.: Exploiting Style in Architectural Design Environments. Proceedings of the ACM SIGSOFT Symposium on Foundations of Software Engineering, New Orleans, 1994.

[52] Garlan D., Monroe R., Wile D.: ACME: An Architecture Description Interchange Language. Proceedings of CASCON'97, Toronto, November 1997.

[53] Garlan D., Monroe R., Wile D.: ACME: Architectural Description of Component-Based Systems. Foundations of Component-Based Systems, Leavens G.T, and Sitaraman M. (Eds.), Cambridge University Press, 2000.

[54] Greenwood M., Balasubramaniam D., Cimpan S., Kirby N.C., Mickan K., Morrison R., Oquendo F., Robertson I., Seet W., Snowdon R., Warboys B., Zirintsis E.:Process Support for Evolving Active Architectures, Proceedings of the 9th European Workshop on Software Process Technology, LNCS 2786, Springer Verlag, Helsinki, September 2003.

[55] Groote J. F., Mateescu R.: Verification of Temporal Properties of Processes in a Setting with Data. Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology, Amazonia, LNCS 1548, January 1999.

[56] Heisel M., Levy N.: Using LOTOS Patterns to Characterize Architectural Styles, Proceedings of the International Conference on Theory and Practice of Software Development, LNCS 1214, Springer Verlag, 1997.

[57] Inverardi P., Wolf A.: Formal Specification an Analysis of Software Architectures using the Chemical Abstract Machine Model. IEEE Transactions on Software Engineering, Vol. 21, No. 4, April 1995.

[58] Inverardi P., Wolf A., Yankelevich D.: Static Checking of System Behaviors using Derived Component Assumptions. ACM Transactions on Software Engineering and Methodology, Vol. 9, No. 3, July 2000.

[59] Kerschbaumer A.: Non-Refinement Transformation of Software Architectures. Proceedings of the ZB2002 International Workshop on Refinement of Critical Systems: Methods, Tools and Experience, Grenoble, Janvier 2002.

[60] Kozen D.: Results on the Propositional μ-Calculus. Theoretical Computer Science 27:333-354, 1983.

[61] Leymonerie F., Cimpan S., Oquendo F. : Extension d'un langage de description architecturale pour la prise en compte des styles architecturaux : application à J2EE. Proceedings of the 14th International Conference on Software and Systems Engineering and their Applications. Paris, December 2001 (In French).

[62] Leymonerie F., Cimpan S., Oquendo F., "État de l'art sur les styles architecturaux : classification et comparaison des langages de description d'architectures logicielles", Revue Génie Logiciel, No. 62, September 2002 (In French).

[63] Luckham D.C., Kenney J.J., Augustin L.M., Vera J., Bryan D., Mann W.: Specification and Analysis of System Architecture Using RAPIDE. IEEE Transactions on Software Engineering, Vol. 21, No. 4, April 1995.

[64] Magee J., Dulay N., Eisenbach S., Kramer J.: Specifying Distributed Software Architectures. Proceedings of the 5th European Software Engineering Conference, Sitges, Spain, September 1995.

[65] Martí-Oliet N., Meseguer J.: Rewriting Logic: Roadmap and Bibliography. Theoretical Computer Science, 2001.

[66] Mateescu R., Garavel H.: XTL: A Meta-Language and Tool for Temporal Logic Model-Checking. Proceedings of the 1st International Workshop on Software Tools for Technology Transfer, Aalborg, Denmark, July 1998.

[67] Medvidovic N., Taylor R.: A Classification and Comparison Framework for Architecture Description Languages. Technical Report UCI-ICS-97-02, Department of Information and Computer Science, University of California. Irvine, February 1997.

[68] Milner R.: Communicating and Mobile Systems: The π-Calculus. Cambridge University Press, 1999.

[69] Monroe R.: Capturing Software Architecture Design Expertise with ARMANI. Technical Report CMU-CS-98-163, Carnegie Mellon University, January 2001.

[70] Moriconi M., Qian X., Riemenschneider R.A.: Correct Architecture Refinement. IEEE Transactions on Software Engineering, Vol. 21, No. 4, April 1995.

[71] Moriconi M., Riemenschneider R.A.: Introduction to SADL 1.0: A Language for Specifying Software Architecture Hierarchies. Computer Science Laboratory, SRI International, Technical Report SRI-CSL-97-01, March 1997.

[72] Morrison R.: On the Development of S-algol. PhD Thesis, University of St Andrews, 1979.

[73] Philipps J., Rumpe B.: Refinement of Pipe and Filter Architectures. Proceedings of FM’99, LNCS 1708, 1999.

[74] RAPIDE Design Team: Guide to the RAPIDE 1.0. Language Reference Manuals, Stanford University, July 1997.

[75] Rongviriyapanish S., Levy N.: Variations sur le Style Architectural Pipe and Filter. Actes du Colloque sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'00), Grenoble, France, January 2000.

[76] Sangiorgi, D., Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD Thesis, University of Edinburgh, 1992.

[77] Stirling C.: Modal and Temporal Properties of Processes. Springer Verlag, 2001.

[78] Stolen K., Broy M.: Specification and Development of Interactive Systems. Springer Verlag, 2001.

[79] Strachey C.: Fundamental Concepts in Programming Languages. Oxford University Press, Oxford, 1967.

[80] Tennent R.D.: Language Design Methods based on Semantic Principles. Acta Informatica 8, 1977.

[81] Wile D.: AML: An Architecture Meta Language. Proceedings of the 14th International Conference on Automated Software Engineering, pp. 183-190. Cocoa Beach. October 1999.

[82] Zirintsis, E.: Towards Simplification of the Software Development Process: The Hyper-code Abstraction. PhD Thesis, University of St Andrews, 2000.

Further information

For further details see the ArchLog group's section of the VALORIA's activity report for 2004-2005.