The concept of model is widely used in the MDE approach in order to represent several software artifacts, which are handled by different development teams throughout the software life cycle. Management of these models requires the definition of a set of model management operators such as the composition operation. This is generally an operation, which is dedicated to merge a number of models in order to create one (or more) incorporated model and which depends on the application context. The current work focuses on the description of a formal approach for model composition where the composition is specified by a set of graph transformation rules over UML-compliant models. The semantics of our composition operator is defined using triple graph grammars (TGGs) formalism. Furthermore, we present a composition scheme interpreted by a three-steps composition process: matching, checking and merging.
This work describes a declarative and lightweight metamodelling framework called uMF for modelling and validating structural constraints on programming language data-structures. By depending solely on the Lua language, uMF is embeddable even in very constrained embedded systems. That way, models can be instantiated and checked close to or even within the final run-time environment, thus permitting validation to take the current state of the system into account. In contrast to classical metamodelling languages such as ECore, uMF supports open world models that are only partially constrained. We illustrate the use of uMF with a real-world example of a robot control formalism and compare it with a previously hand-written implementation. The results indicate that strict formalization was facilitated while flexibility and readability of the constraints were improved.
In the automotive domain software developers are confronted with steadily increasing complexity of models in MATLAB/Simulink. To assist developers with complexity handling, we suggest automatic analyses resulting in special views on Simulink models, e. g. to visualise dependencies of model parts. To this end, we present (1) a modelbased approach based on the Eclipse Modeling Framework (EMF) and model transformations and (2) an alternative approach applying a central database combined with MATLAB/Simulink and Java functionality. We compare the approaches with each other especially in terms of scalability and efficiency.
Design patterns provide a means to reuse proven solutions during development, but also to identify good practices during analysis. These are particularly relevant in complex and critical software, such as is the case of ubiquitous and pervasive systems. Model Driven Engineering (MDE) presents a solution for this problem, with the usage of high level models. As part of an effort to develop approaches to the migration of applications to mobile contexts, this paper reports on a tool that identifies design patterns in source code. Code is transformed into both platform specific and independent models, and from these design patterns are inferred. MapIt, the tool which implements these functionalities is described.
Formal modelling of protocols is often aimed at one specific purpose such as verification or automatically generating an implementation. This leads to models that are useful for one purpose, but not for others. Being able to derive models for verification and implementation from a single model is beneficial both in terms of reduced total modelling effort and confidence that the verification results are valid also for the implementation model. In this paper we introduce the concept of a descriptive specification model and an approach based on refining a descriptive model to target both verification and implementation. Our approach has been developed in the context of the Coloured Petri Nets (CPNs) modelling language. We illustrate our approach by presenting a descriptive specification model of the Websocket protocol which is currently under development by the Internet Engineering Task Force (IETF), and we show how this model can be refined to target both verification and implementation.
A recognized quality of a modern software system is its ability to adapt to changing user needs, user tasks, user skills and context of operation. While recent research results have been achieved in the domain of architectures, requirements and user interfaces, very little attention has been devoted to the adaptation of the data manipulation aspects of the system. However, mobile and pervasive applications impose constraints over the amount of data that can be supported, thus making necessary to adapt the schema to the current context in order to provide only relevant data to the system user. This paper presents a feature-based approach to adapt database schemas according to the changing context conditions. The method allows the derivation of a consistent and sufficient sub-schema starting from the current context. We define and formalize a generic framework, considering two levels of abstraction for database schema specification, and we propose two schema derivation algorithms.
Testing is an established and integral part of the system design and development process, but incomplete coverage still leaves room for potential undiscovered bugs. Runtime verification addresses this issue by integrating verification oracles into the code, allowing for reparatory action to be taken in case of system failure after deployment. Despite the complementarity of the two approaches, the application of the two approaches at different stages in the development and deployment process results in much duplication of effort. In this paper we investigate the combination of the two approaches, by showing how one can use testing oracles to derive correct runtime verification monitors. We show how this can be achieved using QuickCheck and Larva, and apply the resulting framework to Riak, a fault-tolerant distributed database written in Erlang.
This paper focus on the modelling of reactive systems, more particularly, control systems. A set of guidelines is proposed in order to build models that support analysis, simulation and prototyping. The guidelines are split in two parts; the analysis of a problem is addressed first, followed by the design with Coloured Petri Nets (CPNs). A smart library example is used as case study. The models developed under this approach turn out to be modular, parameterisable, configurable and executable.
The widespread use of embedded systems requires the creation of industrial software technology, which will make it possible to engineer systems that are correct by construction. That can be achieved through the use of validated (trusted) components, verification of design models and automatic configuration of applications from validated design models. These guidelines have been instrumental for developing COMDES - a component-based framework for real-time embedded control systems. In this framework, an application is conceived as a network of distributed embedded actors that communicate with one another by means of labeled messages (signals), whereby I/O signals are exchanged with the controlled plant at precisely specified time instants, resulting in the elimination of I/O jitter. The paper presents an analysis method that can be used to validate COMDES design models using the Simulink environment. It is based on a semantics-preserving transformation of a COMDES design model into a Simulink analysis model, which preserves both the functional and timing behaviour of the original design model. The discussion is illustrated with an industrial case study -- a Medical Ventilator Control System, which has been used to validate the developed design and analysis methods.
Domain-specific modelling enables modelling using constructs familiar to experts of a specific domain. Domain-specific models (DSms) can be automatically transformed to various lower-level artifacts such as configuration files, documentation, executable programs and performance models. Although many researchers have tackled the formalization of various aspects of model-driven development such as model versioning, debugging and transformation, very little attention has been focused on formalizing how artifacts are actually synthesized from DSms. State-of-the-art approaches rely on ad hoc coded generators which essentially use modelling tool APIs to programmatically iterate through model entities and produce the final artifacts. In this work, we propose a more structured approach to artifact generation where layered model transformations are used to modularly isolate, compile and re-combine various aspects of DSms. We demonstrate our technique by detailing the synthesis of running Google Android applications from DSms, and discuss how it may be applied in addressing the characteristic non-functional requirements (e.g. timing constraints, resource utilization) of modern embedded systems.
When applying model-based techniques to the engineering of embedded application software, a typical challenge is the complexity of dependencies between application elements. In many situations, e.g., during rollout of products or in the evolution of product lines, the understanding of these dependencies is a key capability. In this paper, we discuss how model-based techniques, in particular, model transformations can help to reduce the complexity of such analysis tasks. To this end, we realised a representation of Simulink models based on the Eclipse Modeling Framework (EMF). The resulting integration allows us to apply various model-based frameworks from the Eclipse ecosystem. On this basis we developed a view that increases the visibility of functional dependencies, which otherwise would have been hidden due to a lack of abstraction in the native Simulink representation. The provided analysis framework comes in handy, when such a model has to be modified. Consequently, the developer is supported in reusing existing models and avoiding errors. The concepts and techniques are illustrated with a running example, which is derived from a real industry model from Automotive Software Engineering.
The development of software product lines with model-driven approaches involves dealing with diverse modeling artifacts such as use case diagrams, component diagrams, class diagrams, activity diagrams, sequence diagrams and others. In this paper we focus on use cases for product line development and we analyze them from the perspective of variability. In that context we explore the UML (Unified Modeling Language) «extend» relationship. We also explore the functional refinement of use cases with «extend» relationships between them. This work allows understanding the activities of use case modeling with support for variability and of use case modeling with functional refinement when variability is present.
The task of programming sensor-based systems comes with severe constraints on the resources, typically memory, CPU power, and energy. The challenge is usually addressed with techniques that result in poor code understandability and maintainability. In this paper, we report on a data centric language extension based on a tuple-space abstraction, akin to Linda [2], applied to PicOS [5], a programming environment for wireless sensor networks (WSN's). The extension improves state and context management in a multi-tasking environment suffering from severe memory limitations. The solution integrates tuple operations into the model -- for networking, event handling, and thread contexts. We demonstrate how tuple constructs improve coding and reduce code overhead. We also show how thread's context-tuples can be used as interface arguments for extension by modular aspect constructs.
In this paper, we present a design space exploration (DSE) method for embedded systems, which represents the design space as a categorical graph product, in order to overcome the challenge of performing multiple DSE activities, such as task mapping, processor allocation, and software binding. Moreover, the method adopts a Model-Driven Engineering (MDE) approach, defining a design space metamodel to represent the categorical graph product and other DSE concepts, such as solutions, costs, and DSE activities. Furthermore, exploiting the MDE approach, we use model-to-model transformation rules to implement the design constraints, which guide and prune the design space. The method is applied to the design of a real-life application, and experiments demonstrate its effectiveness.
This past few years, avionics platform conception changed to integrated architecture, permitting one processor to host some applications, in order to reduce weight and space. But this method entails more complexity, especially in safety domain, while time to market tends to decrease, so new development processes are needed. Model-based approaches are now mature enough to design embedded critical systems and perform architecture exploration. In this paper we present a new modeling approach allowing avionics platform description and dynamic simulation. This method aim at dimensioning the architecture according to the applications it has to process, and to achieve early platform validation.
The Home Automation System (HAS) is a service-oriented application that facilitates the automation of a private home to improve the comfort and security of its residents. HAS is implemented using a service-oriented architecture. Many of the services in the HAS dynamically change their configuration during run-time. This occurs due to change in availability and bindings between services. Dynamic reconfigurations of services in the HAS presents several testing challenges, one being the specification of test oracles. In this paper, we give an approach for specifying test oracles for services in the HAS. We formally specify test oracles in the JML specification language. To verify service behavior in the presence of dynamic reconfigurations, we use mechanisms in the service architecture that notify dynamic changes along with run-time evaluation of JML specifications. We illustrate our approach using an example service in the H-Omega HAS developed on the OSGi™ and iPOJO service platform. To evaluate our approach, we developed a testing framework that allows for generation of tests with dynamic service reconfigurations. In addition, we seeded faults into the example service, and evaluated the effectiveness of the test oracles in revealing the faults using the generated tests.
The scope of Model-Driven Engineering is not limited to Model-Based Development (MBD), i.e. the generation of code from system models, but involves also Model-Based Testing (MBT), which is the automatic generation of efficient test procedures from corresponding test models. Both MBD and MBT include activities such as model creation, model checking, and use of model compilers for the generation of system/test code. By reusing these common activities, the efficiency of MBT can be significantly improved for those organizations which have already adopted MBD, since one of the major efforts in MBT is the creation of test models. In this work, we propose to exploit modeling activity efforts by deriving test models from system models. In this respect, we present a case study in which the Executable and Translatable UML system models are used for automatically generating test models in the QTronic Modeling Language using horizontal model transformations. In turn, the derived artefacts can be used to produce test cases which result to be appropriate for the system under development.
This work presents a Model Driven Engineering (MDE) approach to the generation of a MOF-based internal design representation for an embedded application described using UML class and sequence diagrams. Differently from other similar MDE-based approaches for embedded system design, which translate UML models to some specific internal format, our internal design representation, as a MOF-based metamodel, can take advantage of the concept of transformation between models to implement cosynthesis tools. Our internal design representation captures the specified system as a set of hierarchical modules, interconnected by ports, and processes, which communicate through send/receive operations using channels or through shared variables. The execution flow of the application is also captured by means of a control/data flow graph, which is used as input to a co-synthesis framework for embedded systems design. The paper describes the defined transformations between models and illustrates them with a case study to show the effectiveness of the approach.
A shared Sense-and-Respond infrastructure that is embedded into a physical environment requires considerable run-time support to facilitate the dynamic dispatch and execution of new service instances. Such an infrastructure must also be able to statically analyze new services in order to verify their safety and derive their specific resource requirements (i.e., prior to dispatch). Toward this goal we have developed a multi-dimensional type system for our pervasive sensory service composition language; this formalism extracts implicit constraints from service instances to verify an expanded notion of type safety. While our formal system is rigorous, it is light-weight and essentially transparent to a service programmer. The type-system automatically infers data types that are annotated with a vector of type specific attributes and uses these annotations to establish and verify a range of resource constraints (bounds for computation and memory usage, camera resolution requirements, etc.). In this paper we present an overview of our formal methodology, provide concrete examples of how these formalisms are used in practice (through service logic examples and derived constraint sets) and discuss the details of our implementation.
Model-driven development and verification approaches are highly desirable in embedded systems development since they help identify functional or non-functional issues in the early stage of development when verification complexity is relatively lower than that of the implemented system. Nevertheless, typical model-driven verification approaches focus mainly on functional aspects, leaving the communication behavior largely under-specified. This paper anticipates that understanding and specifying communication mechanism is important in modeling as well as analysis, and suggests a set of communication patterns categorized by the level of abstraction, message handling mechanisms, and buffering strategies. Design of a component may start with the specification of an abstract component with the default communication pattern, which can be recursively verified and refined. Using communication patterns helps us improve the separation of concerns and facilitating smooth transition of a component design from an abstract function-oriented component to a concrete component with detailed communication behavior.
