Mission planning for multi-agent autonomous systems aims to generate feasible and optimal mission plans that satisfy given requirements. In this article, we propose a tool-supported mission-planning methodology that combines (i) a path-planning algorithm for synthesizing path plans that are safe in environments with complex road conditions, and (ii) a task-scheduling method for synthesizing task plans that schedule the tasks in the right and fastest order, taking into account the planned paths. The task-scheduling method is based on model checking, which provides means of automatically generating task execution orders that satisfy the requirements and ensure the correctness and efficiency of the plans by construction. We implement our approach in a tool named MALTA, which offers a user-friendly GUI for configuring mission requirements, a module for path planning, an integration with the model checker UPPAAL, and functions for automatic generation of formal models, and parsing of the execution traces of models. Experiments with the tool demonstrate its applicability and performance in various configurations of an industrial case study of an autonomous quarry. We also show the adaptability of our tool by employing it in a special case of an industrial case study.

Planning is a critical function of multi-agent autonomous systems, which includes path finding and task scheduling. Exhaustive search-based methods such as model checking and algorithmic game theory can solve simple instances of multi-agent planning. However, these methods suffer from state-space explosion when the number of agents is large. Learning-based methods can alleviate this problem, but lack a guarantee of correctness of the results. In this paper, we introduce MoCReL, a new version of our previously proposed method that combines model checking with reinforcement learning in solving the planning problem. The approach takes advantage of reinforcement learning to synthesize path plans and task schedules for large numbers of autonomous agents, and of model checking to verify the correctness of the synthesized strategies. Further, MoCReL can compress large strategies into smaller ones that have down to 0.05% of the original sizes, while preserving their correctness, which we show in this paper. MoCReL is integrated into a new version of Uppaal Stratego that supports calling external libraries when running learning and verification of timed games models.

Abstract Path planning and task scheduling are two challenging problems in the design of multiple autonomous agents. Both problems can be solved by the use of exhaustive search techniques such as model checking and algorithmic game theory. However, model checking suffers from the infamous state-space explosion problem that makes it inefficient at solving the problems when the number of agents is large, which is often the case in realistic scenarios. In this paper, we propose a new version of our novel approach called MCRL that integrates model checking and reinforcement learning to alleviate this scalability limitation. We apply this new technique to synthesize path planning and task scheduling strategies for multiple autonomous agents. Our method is capable of handling a larger number of agents if compared to what is feasibly handled by the model-checking technique alone. Additionally, MCRL also guarantees the correctness of the synthesis results via post-verification. The method is implemented in UPPAAL STRATEGO and leverages our tool MALTA for model generation, such that one can use the method with less effort of model construction and higher efficiency of learning than those of the original MCRL. We demonstrate the feasibility of our approach on an industrial case study: an autonomous quarry, and discuss the strengths and weaknesses of the methods.

Safety requirements describe risk mitigations against failures that may cause catastrophic consequences on human life, environment and facilities. To be able to implement the correct risk mitigations, it is fundamental that safety requirements are defined based on the results issued from the safety analysis. In this paper, we introduce a heuristic approach to elicit safety requirements based on the knowledge about hazard's causes, hazard's sources and hazard's consequences (i.e. hazard's components) acquired during the safety analysis. The proposed approach is based on a Hazard Ontology that is used to structure the knowledge about the hazards identified during the safety analysis in order to make it available and accessible for requirements elicitation. We describe how this information can be used to elicit safety requirements, and provide a guidance to derive the safety requirements which are appropriate to deal with the hazards they mitigate.

Preliminary hazard analysis (PHA) is a key safetyconcerned activity to identify potential hazards. However, since various stakeholders will be involved in the identification process, a common understanding of the nature of hazards among stakeholders, such as what a hazard consists of and how to describe it without ambiguities, is of crucial importance to achieve the goal of PHA. In this work, we propose a hazard modeling language (HML) based on a domain ontology to facilitate the specification of identified hazards. In addition, we present an approach to guide the transformation from natural language hazard descriptions into the HML specification. Finally, an industrial PHA example is used to illustrate the usefulness of our work.

Architectural engineering of embedded systems comprehensively affects both the development processes and the abilities of the systems. Verification of architectural engineering is consequently essential in the development of safety- and missioncritical embedded system to avoid costly and hazardous faults. In this paper, we present the Architecture Quality Assurance Tool (AQAT), an application program developed to provide a holistic, formal, and automatic verification process for architectural engineering of critical embedded systems. AQAT includes architectural model checking, model-based testing, and selective regression verification features to effectively and efficiently detect design faults, implementation faults, and faults created by maintenance modifications. Furthermore, the tool includes a feature that analyzes architectural dependencies, which in addition to providing essential information for impact analyzes of architectural design changes may be used for hazard analysis, such as the identification of potential error propagations, common cause failures, and single point failures. Overviews of both the graphical user interface and the back-end processes of AQAT are presented with a sensor-to-actuator system example.

The Architecture Quality Assurance Framework (AQAF) is a theory developed to provide a holistic and formal verification process for architectural engineering of critical embedded systems. AQAF encompasses integrated architectural model checking, model-based testing, and selective regression verification techniques to achieve this goal. The Architecture Quality Assurance Tool (AQAT) implements the theory of AQAF and enables automated application of the framework. In this paper, we present an evaluation of AQAT and the underlying AQAF theory by means of an industrial case study, where resource efficiency and fault detection effectiveness are the targeted properties of evaluation. The method of fault injection is utilized to guarantee coverage of fault types and to generate a data sample size adequate for statistical analysis. We discovered important areas of improvement in this study, which required further development of the framework before satisfactory results could be achieved. The final results present a 100% fault detection rate at the design level, a 98.5% fault detection rate at the implementation level, and an average increased efficiency of 6.4% with the aid of the selective regression verification technique.

Summary Automated software testing is a critical enabler for modern software development, where rapid feedback on the product quality is expected. To make the testing work well, it is of high importance that impediments related to test automation are prevented and removed quickly. An enabling factor for all types of improvement is to understand the nature of what is to be improved. We have performed a systematic literature review of reported impediments related to software test automation to contribute to this understanding. In this paper, we present the results from the systematic literature review: The list of identified publications, a categorization of identified impediments, and a qualitative discussion of the impediments proposing a socio‐technical system model of the use and implementation of test automation.

The fast development of sensing devices and radios enables more powerful and flexible remote health monitoring systems. Considering the future vision of the Internet of Things (IoT), many requirements and challenges rise to the design and implementation of such systems. Bridging the gap between sensor nodes on the human body and the Internet becomes a challenging task in terms of reliable communications. Additionally, the systems will not only have to provide functionality, but also be highly secure. In this paper, we provide a survey on existing communication protocols and security issues related to pervasive health monitoring, describing their limitations, challenges, and possible solutions. We propose a generic protocol stack design as a first step toward handling interoperability in heterogeneous low-power wireless body area networks.

The environment, where a safety critical system (SCS) operates, is an important source from which safety requirements of the SCS can originate. By treating the system under construction as a black box, the environment is typically documented as a number of assumptions, based on which a set of environmental safety requirements will be elicited. However, it is not a trivial task in practice to capture the environmental assumptions to elicit safety requirements. The lack of certain assumptions or too strict assumptions will either result in incomplete environmental safety requirements or waste many efforts on eliciting incorrect requirements. Moreover, the variety of operating environment for an SCS will further complicate the task, since the captured assumptions are at risk of invalidity, and consequently the elicited requirements need to be revisited to ensure safety has not been compromised by the change. This short paper presents an on-going work aiming to 1) systematically organize the knowledge of system operating environment and, 2) facilitate the elicitation of environmental safety requirements. We propose an ontological approach to achieve the objectives. In particular, we utilize conceptual ontologies to organize the environment knowledge in terms of relevant environment concepts, relations among them and axioms. Environmental assumptions are captured by instantiating the environment ontology. An ontological reasoning mechanism is also provided to support elicitation of safety requirements from the captured assumptions.

To better understand the challenges encountered by users and developers of automatic software testing, we have performed an empirical investigation of a discussion board used for support of a test automation framework having several hundred users. The messages on the discussion board were stratified into problem reports, help requests, development information, and feature requests. The messages in the problem report and help request strata were then sampled and analyzed using thematic analysis, searching for common patterns. Our analysis indicate that a large part of the impediments discussed on the board are related to issues related to the centralized IT environment, and to erroneous behaviour connected to the use of the framework and related components. We also observed a large amount of impediments related to the use of software development tools. Turning to the help requests, we found that the majority of the help requests were about designing test scripts and not about the areas that appear to be most problematic. From our results and previous publications, we see a clear need to simplify the use, installation, and configuration of test systems of this type. The problems attributable to software development tools suggest that testers implementing test automation need more skills in handling those tools, than historically has been assumed. Finally, we propose that further research into the benefits of centralization of tools and IT environments, as well as structured deployment and efficient use of test automation, is performed.

In the modern automotive industry, feature models have been widely used as a domain-specific requirements model, which can capture commonality and variability of a software product line through a set of features. Product variants can thus be configured by selecting different sets of features from the feature model. For feature-oriented requirements validation, the variability of feature sets often makes the hidden flaws such as behavioral inconsistencies of features, hardly to avoid. In this paper, we present an approach to feature-oriented requirements validation for automotive systems w.r.t. both functional behaviors and non-functional properties. Our approach first starts with the behavioral specification of features and the associated requirements by following a restricted use case modeling approach, and then formalizes such specifications by using a formal yet literate language for analysis. We demonstrate the applicability of our approach through an industrial application of a Vehicle Locking-Unlocking system.

Automated test execution is one of the more popular and available strategies to minimize the cost for software testing, and is also becoming one of the central concepts in modern software development as methods such as test-driven development gain popularity. Published studies on test automation indicate that the maintenance and development of test automation tools commonly encounter problems due to unforeseen issues. To further investigate this, we performed a case study on a telecommunication subsystem to seek factors that contribute to inefficiencies in use, maintenance, and development of the automated testing performed within the scope of responsibility of a software design team. A qualitative evaluation of the findings indicates that the main areas of improvement in this case are in the fields of interaction design and general software design principles, as applied to test execution system development.

Designing and developing mission-critical embedded systems is challenging, especially due to additional platform constraints regarding timing and computational resources. The development process of embedded systems should include verification techniques already at the architecture design phase, to provide evidence that a system's architecture fulfills its requirements. The Architecture Analysis and Design Language (AADL) is used to model the system's architecture. Among others, the language contains a Behavior Annex, for describing the behavior of an AADL model, at an abstract level. In this paper, we present a verification tool, called ABV, tailored for AADL models with a behavioral annex. Given an architecture defined in AADL and its behavior specified in the associated language, our tool model-checks the latter against the requirements specified in Computation Tree Logic (CTL). ABV is based on AADL's formal denotational semantics implemented in Standard ML, and is encapsulated into an Eclipse plug-in based on the OSATE platform. The tool has been applied on the Production Cell case study, which is briefly described in the paper.

Agile methods hold a significant promise to reduce cycle times and provide greater value to all key stakeholders involved in the software ecosystem. While these methods appear to be well suited for embedded systems development, their use has not become a widespread practice. In analyzing the state-of-the-art, as captured in published literature, we found that there are technical issues (requirements management, and testing), as well as organizational issues (process tailoring, knowledge sharing & transfer, culture change, and support infrastructure). In this paper, we build preliminary guidance for firms around these six areas and presented as a framework that will enable understanding the expected adoption trajectory.

Openness and trust are key elements to sustaining any successful client-supplier relationship. When the relationship is transitioning from being arms-length to evolving into a true partnership, it is critical to establish a shared understanding of not only the current state, but also of the expected future state. A workshop organized and facilitated by a neutral party, with the senior leadership of both organizations provides an ideal means for articulating implicit assumptions and surfacing hidden challenges such that an actionable vision can be created. Using a recent workshop held with both EuroTel and IndiaCo, the key elements of the workshop are discussed, along with the lessons learned. Moreover, this workshop provides further insight into the mechanics of the evolution and governance of outsourcing relationships.

Summary form only given, as follows. The complete presentation was not made available for publication as part of the conference proceedings. The Hi-Five framework is a holistic framework for the validation and verification of embedded real-time systems. The framework reuses the state of the art in formal verification and test case generation to provide an end-to-end solution to mitigate the typically high cost of validation and verification activities. The framework is based on a literate formal specification language, the Timed Abstract State Machine (TASM) language. The TASM language captures the three key aspects of embedded real-time system behavior, namely functional behavior, timing, and resource consumption. These aspects can be captured and analyzed using the TASM language and its associated toolset. Using the TASM language, the Hi-Five framework models systems at multiple levels of abstraction and provides traceability between related models. The framework provides an overarching approach to system engineering by leveraging the formal semantics of the TASM language to automate verification and test case generation. During the early phases of system engineering, incorporating nonfunctional properties in system models is an approximate activity at best. For example, before an implementation exists, it is challenging to specify behavior related to time and resource consumption. Nevertheless, gaining insight into the system designs, before the system is implemented, yields considerable benefits in terms of cost and time savings. For example, evaluating design properties, such as end-to-end latency and Quality of Service can help optimize designs or select between competing designs. The Hi-Five approach to resolving this apparent paradox is to use bi-directional traceability through levels of abstraction. The end result of the approach is an integrated development environment where the effect of changes can be efficiently managed and enforced through levels of abstraction, from requirements to implementation.

In this paper, we present some of the issues encountered when trying to apply model-driven approaches to the engineering of real-time systems. In real-time systems, quantitative values of time, as reflected through the duration of actions, are central to the system's correctness. We review basic time concepts and explain how time is handled in different modeling languages. We expose the inherent paradox of incorporating quantitative time-dependent behavior in high-level models. High-level models are typically built before the system is implemented, which makes quantitative time metrics difficult to predict since these metrics depend heavily on implementation details. We provide some possible answers to this paradox and explain how the Timed Abstract State Machine (TASM) language helps address some of these issues.

Recreating the context in which software processes are developed is difficult in the undergraduate classroom environment. As a result, traditional lecture-based teaching approaches do not necessarily translate into long-term understanding of software processes. To give students a deeper appreciation for the strengths and weaknesses of software process models, we designed the software process simulation game using constructivism as the underlying foundation. In this paper, we discuss the challenges associated with teaching software processes models, provide an overview of the game, detail its mechanics, and discuss the lessons learned from playing the game. Since the game does not involve actual programming or design activities, it can be used effectively for teaching both novice and experienced software engineers.

Software is a critical component of mission capability in all aerospace systems. This capability is realized directly through the use of onboard software, and enabled through the use of software on ground support systems. Students attending an aerospace engineering program come with a highly diversified background in software development ranging from novice user to expert programmer. A first course in software development has to account for the diversity, and as an outcome provide both a common vocabulary, as well as a common baseline of skills. This paper presents our learning from designing and teaching such a course for aerospace engineering undergraduates

The traditional approach to high-integrity embedded system development has been to develop and verify the application with the assumption that either the operating system services have deterministic behaviour with well understood operational semantics or that the operating system itself is certified. Formal verification approaches have focused on modelling the application at the right level of abstraction and verifying specific properties based on the model. The effective use of formal methods in high-integrity embedded system development requires efficient models of both the application and the underlying operating system services. Software implemented operating systems pose significant complexity constraints in terms of creating usable models. This paper presents a component-based formal model of a hardware-implemented run-time kernel. It builds on work carried out earlier for the LAMR kernel (K. Lundqvist and L. Asplund, 2003). The components are designed to allow easy deployment, and can be replicated to enable system growth. Additionally, the kernel presented in this paper supports multiprocessor scheduling.

The readability of formal requirements specification languages is hypothesized as a limiting factor in the acceptance of formal methods by the industrial community. An empirical study was conducted to determine how various factors of state-based requirements specification language design affect readability using aerospace applications. Six factors were tested in all, including the representation of the overall state machine structure, the expression of triggering conditions, the use of macros, the use of internal broadcast events, the use of hierarchies, and transition perspective (going-to or coming-from). Subjects included computer scientists as well as aerospace engineers in an effort to determine whether background affects notational preferences. Because so little previous experimentation on this topic exists on which to build hypotheses, the study was designed as a preliminary exploration of what factors are most important with respect to readability. It can serve as a starting point for more thorough and carefully controlled experimentation in specification language readability.