A Compositional Semantics of UML-RSDS

This paper provides a semantics for the UML-RSDS (Reactive System Development Support) subset of UML, using the real-time action logic (RAL) formalism. We show how this semantics can be used to resolve some ambiguities and omissions in UML semantics, and to support reasoning about specifications using the B formal method and tools. We use `semantic profiles' to provide precise semantics for different semantic variation points of UML. We also show how RAL can be used to give a semantics to notations for real-time specification in UML. Unlike other approaches to UML semantics, which concentrate on the class diagram notation, our semantic representation has behaviour as a central element, and can be used to define semantics for use cases, state machines and interactions, in addition to class diagrams.

Describing Web Service Architectures through Design-by-Contract

Architectural description languages (ADLs) are used to specify a high-level, compositional view of a software application, specifying how a system is to be composed from coarse-grain components. ADLs usually come equipped with a formal dynamic semantics, facilitating specification and analysis of distributed and event-based systems. In this paper, we describe the TrustME, an ADL framework that provides both a process and a structural view of web service-based systems. We use Petri-net descriptions to give a dynamic view of business workflow for web service collaboration. We adapt the approach of Schmidt to define a form of Meyer's design-by-contract for configuring workflow architectures. This serves as a configuration-level means of constructing safer, more robust systems.

An Architectural Description Language for Enterprise Computing

Architectural description languages (ADLs) are used to specify high-level, compositional view of a software application. ADLs usually come equipped with a rigourous state-transition style semantics, facilitating specification and analysis of distributed and event-based systems. However, enterprise system architectures built upon newer middleware (implementations of Java’s EJB specification, or Microsoft’s COM+/ .NET) require additional expressive power from an ADL. The TrustME ADL is designed to meet this need. In this paper, we describe several aspects of TrustME that facilitate specification and anlysis of middleware-based architectures for the enterprise.

Trust-By-Contract: Modelling, Analysing and Predicting Behaviour in Software Architectures

Architecture description languages (ADLs) are used to specify high-level, compositional views of a software application. ADL research focuses on software composed of prefabricated parts, so-called software components. ADLs usually come equipped with rigorous state-transition style semantics, facilitating verification and analysis of specifications. Consequently, ADLs are well suited to configuring distributed and event-based systems. However, additional expressive power is required for the description of enterprise software architectures – in particular, those built upon newer middleware, such as implementations of Java’s EJB specification, or Microsoft’s COM+/.NET. The enterprise requires distributed software solutions that are scalable, business-oriented and mission-critical. We can make progress toward attaining these qualities at various stages of the software development process. In particular, progress at the architectural level can be leveraged through use of an ADL that incorporates trust and dependability analysis. Also, current industry approaches to enterprise development do not address several important architectural design issues. The TrustME ADL is designed to meet these requirements, through combining approaches to software architecture specification with rigorous design-by-contract ideas. In this paper, we focus on several aspects of TrustME that facilitate specification and analysis of middleware-based architectures for trusted enterprise computing systems.

Stratified resolution

We introduce a calculus of stratified resolution, in which special attention is paid to clauses that "define" relations. If such clauses are discovered in the initial set of clauses, they are treated using the rule of definition unfolding, i.e. the rule that replaces defined relations by their definitions. Stratified resolution comes with a powerful notion of redundancy: a clause to which definition unfolding has been applied can be removed from the search space. To prove the completeness of stratified resolution with redundancies, we use a novel combination of Bachmair and Ganzingerâ??s model construction technique and a hierarchical construction of orderings and least fixpoints.

Compositional Model Repositories via Dynamic Constraint Satisfaction with Order-of-Magnitude Preferences

The predominant knowledge-based approach to automated model construction, compositional modelling, employs a set of models of particular functional components. Its inference mechanism takes a scenario describing the constituent interacting components of a system and translates it into a useful mathematical model. This paper presents a novel compositional modelling approach aimed at building model repositories. It furthers the field in two respects. Firstly, it expands the application domain of compositional modelling to systems that can not be easily described in terms of interacting functional components, such as ecological systems. Secondly, it enables the incorporation of user preferences into the model selection process. These features are achieved by casting the compositional modelling problem as an activity-based dynamic preference constraint satisfaction problem, where the dynamic constraints describe the restrictions imposed over the composition of partial models and the preferences correspond to those of the user of the automated modeller. In addition, the preference levels are represented through the use of symbolic values that differ in orders of magnitude.