The relationship between states (status of a system) and modes (capabilities of a system) used to describe system requirements is often poorly defined. The unclear relationship could make systems of interest out of control because of the out of boundaries of the systems caused by the newly added modes. Formally modeling and verifying requirements can clarify the relationship, making the system safer. To this end, an innovative approach to analyzing requirements is proposed. The MoSt language (a Domain Specific Language implemented on the Xtext framework) is firstly designed for requirements modeling and a model validator is realized to check requirements statically. A code generator is then provided to realize the automatic model transformation from the MoSt model to a NuSMV model, laying the foundation for the dynamic checks of requirements through symbolic model checking. Next, a NuSMV runner is designed to connect the NuSMV with the validator to automate the whole dynamic checks. The grammar, the model validator, the code generator, and the NuSMV runner are finally integrated into a publicly available Eclipse-based tool. Two case studies have been employed to illustrate the feasibility of our approach. For each case study, we injected 14 errors. The results show that the static and dynamic checks can successfully detect all the errors.

Traditional requirements engineering does not benefit from modern software development techniques. The goal of this tutorial is to revisit requirements elicitation and to bridge the gap between traditional requirements engineering and modern software development. This tutorial will provide the attendees with concrete and immediately applicable guidance by demonstrating how to operationalize a fully-fledged toolchain going from user stories to automated acceptance testing using open-source tools.

Ambient environments consist of components surrounding the user and offering services.Applications can here be composed opportunistically and automatically by an intelligent system that puts together available components.Thus, applications that are a priori unknown emerge from the environment.The problem is in the intelligible presentation to an average user of those emerging composite applications.Our approach consists in automatic generation of user-oriented application descriptions from unit descriptions of each component and service.For that, we propose a well-defined language for component description and a method for combining descriptions.A prototype has been developed and used to experiment the generation of different composite application descriptions.Based on these experiments, we assess the degree of fulfillment of the requirements we have identified for the problem.

The RE'18 theme is: "Crossing Boundaries and Increasing Impact". In this context we propose a tutorial on Requirements in an Agile context that aims at exploring the boundaries between requirements, specifications, stories, scenarios and tests. It follows the recent work started in the RE community about agility, from a practical point of view.

Securing critical systems such as Cyber-Physical Systems (CPS) is an important feature especially when it comes to critical transmitted data in a real-time environment. At the same time, the implementation of security counter-measures in such systems may impact transmission delays of critical tasks. For this reason selecting proper security mechanisms in such critical systems is an important issue. In this context, we propose a model-based approach for selecting proper security solution alternatives composed of security patterns at early design stage against real-time requirements. We provide a generalizable and tool-supported solution to support the approach using UML and its profiles. A validation of the work is presented via a simplified version of SCADA (Supervisory Control and Data Acquisition) system case study.

Various disciplines use models for different purposes. While engineering models, including software engineering models, are often developed to guide the construction of a nonexistent system, scientific models, in contrast, are created to better understand a natural phenomenon (i.e., an already existing system). An engineering model may incorporate scientific models to build a system. Both engineering and scientific models have been used to support sustainability, but largely in a loosely-coupled fashion, independently developed and maintained from each other. Due to the inherent complex nature of sustainability that must balance trade-offs between social, environmental, and economic concerns, modeling challenges abound for both the scientific and engineering disciplines. This paper offers a vision that synergistically combines engineering and scientific models to enable broader engagement of society for addressing sustainability concerns, informed decision-making based on more-accessible scientific models and data, and automated feedback to the engineering models to support dynamic adaptation of sustainability systems. To support this vision, we identify a number of research challenges to be addressed with particular emphasis on the socio-technical benefits of modeling.

The Systems Modeling Language (SysML) is a popular and standardized UML profile for systems engineering applications. In addition to seven conventional UML diagram types, SysML supports requirement diagrams and tables that can be used to capture requirements, their attributes, and their relationships. However, several important concepts such as goals and contributions are not predefined in SysML, hindering the reasoning about tradeoffs and adaptation, especially in emerging socio-cyber-physical systems such as smart cities. In this paper, we provide a preliminary investigation of different ways of combining SysML with the User Requirements Notation (URN), a standard that focuses on the modeling and analysis of goals and scenarios. We argue that SysML and URN are complementary and synergistic, and that their combination enables new requirements modeling, analysis, and management opportunities for new types of systems. Examples of potential integration approaches are discussed, briefly assessed, and illustrated with existing tools for SysML, URN, and requirements management.

Development processes for software construction are common knowledge and widely used in most development organizations. Unfortunately, these processes often offer only little or no support in order to meet security requirements. In our work, we propose a methodology to enhance these process models with security concepts, backed by a security-oriented process model specification language. The methodology supports existing process models, which will be extended by established security approaches, as well as information security risk management standards, to fulfill the demand for secure software engineering. The methodology and the process modeling language we propose, have been successfully evaluated by the TERESA project for specifying development processes for trusted applications and integrating security concepts into existing process models.

The model composition provides support to build systems based on a set of less complex sub-models. This operation allows managing complexity while supporting the modularity and reusability tasks. Due to the increase number of the involving models, their composition becomes a tedious task. For that, the need for maintaining traceability information is raised to help managing the composition operation. We propose in this work a graph-based model transformations approach, which aims to keep track of the model composition operation. Our objective is to capture traces in an automatic and reusable manner. Finally, a composition scenario is given to demonstrate the feasibility of our proposal.

Formal methods provide tools to verify the consistency and correctness of a specification with respect to the desired properties of the system. This verification is important as the development of an AAL (Ambient Assisted Living) system involves different technologies (medical services, surveillance cameras, intelligent devices, etc.) requiring a strong consistency checking between models. We illustrate in this paper how we prove some of the properties of the system before the development even starts. To model the AAL system, we use the SysML language. In terms of tools, we used Rational Rhapsody in combination with the OMEGA2 profile which is an executable Uml/SysML profile used for the formal specification and validation of critical real-time systems. This profile is supported by the IFx toolset which provides mechanisms for the model simulation and properties verification of the AAL system.

Self-adaptive systems have the capability to autonomously modify their behaviour at run-time in response to changes in their environment. Self-adaptation is particularly necessary for applications that must run continuously, even under adverse conditions and changing requirements; sample domains include automotive systems, telecommunications, and environmental monitoring systems. While a few techniques have been developed to support the monitoring and analysis of requirements for adaptive systems, limited attention has been paid to the actual creation and specification of requirements of self-adaptive systems. As a result, self-adaptivity is often constructed in an ad-hoc manner. In this paper, we argue that a more rigorous treatment of requirements explicitly relating to self-adaptivity is needed and that, in particular, requirements languages for self-adaptive systems should include explicit constructs for specifying and dealing with the uncertainty inherent in self-adaptive systems. We present RELAX, a new requirements language for self-adaptive systems and illustrate it using examples from the smart home domain.

Software components embedded in ubiquitous systems, especially those using wireless networking, are subject to unpredictable behaviors inherent to using these systems in the physical world. This calls for a runtime management infrastructure to observe and control the components' states and consequently their resulting behaviors. In this paper, we propose a framework for remotely administrating the functional behaviors of software components deployed on wireless devices. This framework is based on components locally managed by internal managers. At the crossroads of the administration system and the wireless application itself, these internal managers master the components' actions by interpreting executable models which themself implement the components' expected behaviors. Besides, high-level managers define and apply management policies to the application's global behavior through the use of these internal managers. Such a coordination occurs through composition.

A formal definition for the semantics of the Whole-Part relationship in the Unified Modeling Language or UML is introduced. This provides a fully directly usable specification which can be incorporated into version 2.0 of UML. An improvement to the current metamodel fragment relating to relationships is proposed, supplemented by the introduction of axioms expressed in the Object Constraint Language or OCL. The overall formalization relates to a clear and concise emphasis on carefully enunciated (primary) characteristics that apply to all instances of a new Whole-Part metatype. Specific kinds of the Whole-Part relationship are defined in terms of secondary characteristics, which must be possessed by subtypes: In UML 1.4, these are Aggregation (a.k.a. white diamond) and Composition (a.k.a. black diamond). Primary and secondary characteristics may then be consistently combined with each other. Consequently, this allows the possible introduction of supplementary forms of Whole-Part. Such a revision is necessary since Aggregation and Composition in UML 1.4 do not cover the full spectrum of Whole-Part theory.

The Fusion and Syntropy object-oriented methods reflect some of the most rigorous object-oriented modelling concepts and experiences currently available. In this paper we identify similarities and differences between the two methods, and discuss how the best concepts from each of these methods can be combined to obtain clearer, more precise analysis models, specifications, and designs, and can be used to enhance the modelling power of the other. A summary of a semantics for Syntropy is given in Appendix A, and ways in which this can be extended to Fusion are described. This work was carried out as part of the EPSRC projects ‘Object-oriented Specification of Reactive and Real-time Systems’ concerning the extension of Fusion to treat reactive systems, and ‘Formal Underpinnings for Object Technology’ concerned with developing a full semantics for Syntropy.

We present techniques for constructing Z specifications from the analysis and design models of the Fusion method. We show how the specifications can be used to more closely tie the Fusion models together. In particular, we outline how the specifications can be used to support rigorous verification of Fusion design models against analysis models.

The difficult task of developing safety-critical systems requires the use of methods and tools that allow developers to manage inherent complexity and to meticulously specify, implement, and analyze desired behavior. Development environments based on formal specification techniques supported by CASE tools can facilitate quality development of such systems. We present our proposed environment for the development of high-assurance systems. The environment provides CASE support for developing and analyzing graphical and formal representations of system structure and behavior. We illustrate the use of the environment with a traffic control system.