Supporting UML-based development of embedded systems by formal techniques

We describe an approach to support UML-based development of embedded systems by formal techniques. A subset of UML is extended with timing annotations and given a formal semantics. UML models are translated, via XMI, to the input format of formal tools, to allow timed and non-timed model checking and interactive theorem proving. Moreover, the Play-Engine tool is used to execute and analyze requirements by means of live sequence charts. We apply the approach to a part of an industrial case study, the MARS system, and report about the experiences, results and conclusions. This work has been supported by EU-project IST 33522 – OMEGA “Correct Development of Real-Time Embedded Systems in UML”. For more information, see . During this project, the second author was at theWeizmann Institute of Science, the third author at VERIMAG, the fourth author at OFFIS, and the fifth author at NLR.     

A real-time profile for UML

This paper describes an approach for real-time modelling in UML, focusing on analysis and verification of time and scheduling-related properties. To this aim, a concrete UML profile, called the ωprofile, is defined, dedicated to real-time modelling by identifying a set of relevant concepts for real-time modelling which can be considered as a refinement of the standard SPT profile. The profile is based on a rich concept of event representing an instant of state change, and allows the expression of duration constraints between occurrences of events. These constraints can be provided in the form of OCL-like expressions annotating the specification or by means of state machines, stereotyped as ‘observers’. A framework for modelling scheduling issues is obtained by adding a notion of resource and a notion of execution time. For proving the relevance of these choices, the profile has been implemented in a validation tool and applied to case studies. It has a formal semantics and is sufficiently general and expressive to define a semantic underpinning for other real-time profiles of UML which in general define more restricted frameworks. In particular, most existing profiles handling real-time issues define a number of predefined attributes representing particular durations or constraints on them and their semantic interpretation can be expressed in the OMEGA-RT profile. This work has been partially supported by the IST-2002-33522 OMEGA project. VERIMAG is an academic research laboratory associated with CNRS, Université Joseph Fourier and Institut Nationale Polytechnique de Grenoble.     

Heap-abstraction for an object-oriented calculus with thread classes

This paper formalizes an open semantics for a calculus featuring thread classes, where the environment, consisting in particular of an overapproximation of the heap topology, is abstractly represented. From an observational point of view, considering classes as part of a component makes instantiation a possible interaction between com- ponent and environment or observer. For thread classes it means that a component may create external activity, which influences what can be observed. The fact that cross-border instantiation is possible requires that the connectivity of the objects needs to be incorporated into the semantics. We extend our prior work not only by adding thread classes, but also in that thread names may be communicated, which means that the semantics needs to account explicitly for the possible acquaintance of objects with threads. We show soundness of the abstraction. Part of this work has been financially supported by the NWO/DFG project Mobi-J (RO 1122/9-4), by the DFG project AVACS (SFB/TR-14-AVACS), by the EU-project IST-33826 Credo: Modeling and analysis of evolutionary structures for distributed services (see )     

A formal framework for software product lines

ContextA Software Product Line is a set of software systems that are built from a common set of features. These systems are developed in a prescribed way and they can be adapted to fit the needs of customers. Feature models specify the properties of the systems that are meaningful to customers. A semantics that models the feature level has the potential to support the automatic analysis of entire software product lines.ObjectiveThe objective of this paper is to define a formal framework for Software Product Lines. This framework needs to be general enough to provide a formal semantics for existing frameworks like FODA (Feature Oriented Domain Analysis), but also to be easily adaptable to new problems.MethodWe define an algebraic language, called SPLA, to describe Software Product Lines. We provide the semantics for the algebra in three different ways. The approach followed to give the semantics is inspired by the semantics of process algebras. First we define an operational semantics, next a denotational semantics, and finally an axiomatic semantics. We also have defined a representation of the algebra into propositional logic.ResultsWe prove that the three semantics are equivalent. We also show how FODA diagrams can be automatically translated into SPLA. Furthermore, we have developed our tool, called AT, that implements the formal framework presented in this paper. This tool uses a SAT-solver to check the satisfiability of an SPL.ConclusionThis paper defines a general formal framework for software product lines. We have defined three different semantics that are equivalent; this means that depending on the context we can choose the most convenient approach: operational, denotational or axiomatic. The framework is flexible enough because it is closely related to process algebras. Process algebras are a well-known paradigm for which many extensions have been defined.     

Object-Z: A specification language advocated for the description of standards

The importance of formalising the specification of standards has been recognised for a number of years. This paper advocates the use of the formal specification language Object-Z in the definition of standards. Object-Z is an extension to the Z language specifically to facilitate specification in an object-oriented style. First, the syntax and semantics of Object-Z are described informally. Then the use of Object-Z in formalising standards is demonstrated by presenting a case study based on the ODP Trader. Finally, a formal semantics is introduced that suggests an approach to the standardisation of Object-Z itself. Because standards are typically large complex systems, the extra structuring afforded by the Object-Z class construct and operation expressions enables the various hierarchical relationships and the communication between objects in a system to be succinctly specified.     

Behavioural specification for hierarchical object composition

Behavioural specification based on hidden (sorted) algebra constitutes one of the most promising recently developed formal specification and verification paradigms for system development.Here we formally introduce novel concepts of behavioural object and equivalence between behavioural objects within the hidden algebra framework. We formally define several object composition operators on behavioural objects corresponding to the hierarchical object composition methodology introduced by CafeOBJ. We study their basic semantical properties and show that our most general form of behavioural object composition with synchronisation has final semantics and a composability property of behavioural equivalence supporting a high reusability of verifications. We also show the commutativity and the associativity of parallel compositions without synchronisation.     

Temporal Semantics for Concurrent M M

Concurrent is a programming language based on the notion of concurrent, communicating objects, where each object directly executes a specification given in temporal logic, and communicates with other objects using asynchronous broadcast message-passing. Thus, Concurrent represents a combination of the direct execution of temporal specifications, together with a novel model of concurrent computation. In contrast to the notions of predicates as processes and stream parallelism seen in concurrent logic languages, Concurrent represents a more coarse-grained approach, where an object consists of a set of logical rules and communication is achieved by the evaluation of certain types of predicate. Representing concurrent systems as groups of such objects provides a powerful tool for modelling complex reactive systems. In order to reason about the behaviour of Concurrent systems, we requir a suitable semantics. Being based upon executable temporal logic, objects in isolation have an intuitive semantics. However, the addition of both operational constraints upon the object's execution and global constraints provided by the asynchronous model of concurrency and communication, complicates the overall semantics of networks of objects. It is this, more complex, semantics that we address here, where temporal semantics for varieties of Concurrent are provided.     

LSC Verification for UML Models with Unbounded Creation and Destruction

The approaches to automatic formal verification of UML models known up to now require a finite bound on the number of objects existing at each point in time. In [W. Damm, B. Westphal, Live and let die: LSC-based verification of UML-models, Science of of Computer Programming 55 (2005) 117–159] we have observed that the class of hardware systems with replicated components studied by McMillan [K.L. McMillan, A methodology for hardware verification using compositional model checking, Science of Computer Programming 37 (2000) 279–309] is equivalent to the class of systems where the only source of infiniteness is unbounded creation and destruction of objects, i.e. where all data-types except for object identities are finite. Exploiting the symmetry of UML models induced by objects being instances of classes, the restriction to finite bounds can be overcome applying [K.L. McMillan, A methodology for hardware verification using compositional model checking, Science of Computer Programming 37 (2000) 279–309].In this paper we report on experiences from an evaluation of this approach within the UML Verifi- cation Environment (UVE) [I. Schinz, T. Toben, C. Mrugalla and B. Westphal, The Rhapsody UML Verification Environment, in: J.R. Cuellar and Z. Liu, editors, Proceedings SEFM 2004 (2004), pp. 174–183], a state-of-the-art tool for formal verification of UML models using Live Sequence Charts (LSC) [W. Damm, D. Harel, LSCs: Breathing Life into Message Sequence Charts, Formal Methods in System Design 19 (2001) 45–80] for requirements specification.     

A layered semantics for a parallel object-oriented language

We develop a denotational semantics for POOL, a parallel object-oriented programming language. The main contribution of this semantics is an accurate mathematical model of the most important concept in object-oriented programming: the object. This is achieved by structuring the semantics in layers working at three different levels: for statements, objects and programs. For each of these levels we define a specialized mathematical domain of processes, which we use to assign a meaning to each language construct. This is done in the mathematical framework of complete metric spaces. We also define operators that translate between these domains. At the program level we give a precise definition of the observable input/output behaviour of a particular program, which could be used at a later stage to decide the issue of full abstractness. We illustrate our semantic techniques by first applying them to a toy language similar to CSP.This paper describes work done in ESPRIT Basic Research Action 3020,Integration.     

OWL-S的形式语义

本文分析了目前语义Web服务的研究现状和存在的问题,特别是语义web服务描述本体OWL-S的形式语义研究中存在的问题,在Srini Narayanan等人研究的基础上,用情景演算理论进一步研完了OWL—S中组合服务描述的形式语义,从而完善了OWL—S的形式语义,为语义Web服务提供了合理的理论基础。     

A blocking model for reactive objects

Objects can be viewed as entities reacting concurrently with their environment through the sending and receiving of messages. In this paper a model for such reactive objects is constructed where messages may be blocked either by the object or by the environment. This model differentiates between output messages controlled by the object, and input messages controlled by the environment. The model is applied to define an object compatibility lattice structure enabling the construction of objects satisfying best possible compatibility requirements.     

Concurrency and Refinement in the Unified Modeling Language

This paper defines a formal semantics for a subset of the Unified Modeling Language (UML). It shows how suitable combinations of class, object, state, and sequence diagrams can be associated with patterns of interaction, expressed in the event notation of Communicating Sequential Processes (CSP). The diagram semantics is then extended to give a meaning to complete models – suitable combinations of diagrams – and thus a concurrency semantics for object models written in UML. This model semantics is in turn used to define a theory of refinement, based upon existing notions of data and process refinement.     

Assert and negate revisited: Modal semantics for UML sequence diagrams

Live Sequence Charts (LSC) extend Message Sequence Charts (MSC), mainly by distinguishing possible from necessary behavior. They thus enable the specification of rich multi-modal scenario-based properties, such as mandatory, possible and forbidden scenarios. The sequence diagrams of UML 2.0 enrich those of previous versions of UML by two new operators, assert and negate, for specifying required and forbidden behaviors, which appear to have been inspired by LSC. The UML 2.0 semantics of sequence diagrams, however, being based on pairs of valid and invalid sets of traces, is inadequate, and prevents the new operators from being used effectively. We propose an extension of, and a different semantics for this UML language—Modal Sequence Diagrams (MSD)—based on the universal/existential modal semantics of LSC. In particular, in MSD assert and negate are really modalities, not operators. We define MSD as a UML 2.0 profile, thus paving the way to apply formal verification, synthesis, and scenario-based execution techniques from LSC to the mainstream UML standard. Preliminary version appeared in SCESM '06: Proc. of the 2006 Int. workshop on Scenarios and State Machines, Shanghai, China (May 2006) [15]. This research was supported by the Israel Science Foundation (grant No.287/02-1), and by The John von Neumann Minerva Center for the Development of Reactive Systems at the Weizmann Institute of Science.     

Knowledge modeling for design decisions

In this paper, we share our experience in modeling and representing design knowledge relevant for engineering design decisions. We define an object model where classes are used to capture design standards and requirements relevant to designed objects. The traditional object model is customized to the representation of design knowledge in two major ways: (1) Classes representing design objects are augmented with design validation information. (2) Associations between classes are made explicit and used to reduce the redundancy and maintain the consistency of the knowledge. We define the semantics of the resulting object model and formulate the axioms that define its consistency. The object model is defined in the context of stamping design knowledge.     

Abstract Interaction Objects

The concept of an ‘interactor’ has been introduced by Faconti and Paterno' [6] as an abstraction of an entity in interactive graphics capable of both input and output. However the notion of interaction object need not be confined to graphics systems; it represents a useful structure for thinking and reasoning about the behaviour of interactive systems in general. As part of Esprit Basic Research Action 7040 (Amodeus-2) we are using the concept of interactor, and existing work on state-based processes and agents, to develop a model and theory of interactive systems. In this paper we describe two formal models for interaction objects and sketch how they can be used to build a small vocabulary of operators to support the rigorous specification of a graphics system. Our model differs from the approach of Faconti and Paterno' in that it abstracts away from any specific graphics framework and is thus suited to the level of abstraction demanded by formal approaches to system development.     

Image Indexing and Retrieval Using Object-based Point Feature Maps

Multimedia data such as audios, images, and videos are semantically richer than standard alphanumeric data. Because of the nature of images as combinations of objects, content-based image retrieval should allow users to query by image objects with finer granularity than a whole image. In this paper, we address a web-based object-based image retrieval (OBIR) system . Its prototype implementation particularly explores image indexing and retrieval using object-based point feature maps. An important contribution of this work is its ability to allow a user to easily incorporate both low- and high-level semantics into an image query. This is accomplished through the inclusion of the spatial distribution of point-based image object features, the spatial distribution of the image objects themselves, and image object class identifiers. We introduce a generic image model, give our ideas on how to represent the low- and high-level semantics of an image object, discuss our notion of image object similarity, and define four types of image queries supported by the OBIR system. We also propose an application of our approach to neurological surgery training.     

一种基于共代数的面向对象形式语义

针对面向对象方法的数学理论基础相对薄弱的问题,利用共代数方法从范畴论及观察的角度研究面向对象的形式语义及行为关系。首先,给出类和对象的共代数描述,其中抽象类定义成一个类规范,类定义为满足类规范的共代数,类的各个对象则看成共代数状态空间上的元素,并分别利用强Monads理论和断言给出方法的行为的参数化描述和语义约束;接着,利用共代数互模拟探讨了不同对象在强Monads下的行为等价关系;最后用实例说明如何通过PVS工具证明类规范的一致性及对象的行为关系。     

Inductive assertions and operational semantics

This paper shows how classic inductive assertions can be used in conjunction with a formal operational semantics to prove partial correctness properties of programs. The method imposes only the proof obligations that would be produced by a verification condition generator – but does not require the definition of a verification condition generator. All that is required is a theorem prover, a formal operational semantics, and the object program with appropriate assertions at user-selected cut points. The verification conditions are generated in the course of the theorem-proving process by straightforward symbolic evaluation of the formal operational semantics. The technique is demonstrated by proving the partial correctness of simple bytecode programs with respect to a preexisting operational model of the Java Virtual Machine.     

Multimedia Data Modeling Through a Semantic View Mechanism

The semantics of multimedia data, which features context-dependency and media-independency, is of vital importance to multimedia applications but inadequately supported by the state-of-the-art database technology. In this paper, we address this problem by proposing MediaView as an extended object-oriented view mechanism to bridge the “semantic gap” between conventional databases and semantics-intensive multimedia applications. This mechanism captures the dynamic semantics of multimedia using a modelling construct named media view, which formulates a customized context where heterogeneous media objects with similar/related semantics are characterized by additional properties and user-defined semantic relationships. Due to the complex ingredients and dynamic application requirements of multimedia databases, it is however difficult for users to define by themselves individual media views in a top–down fashion. To this end, a unique approach of constructing media views logically is devised. In addition, a set of user level operators is defined and implemented to accommodate the specialization and generalization relationships among the views. The usefulness and elegancy of MediaView are demonstrated by its application in a multi-modal information retrieval system. Main part of the work by this Qing Li was done when he was on leave from City University of Hong Kong, HKSAR, China.