Early verification and validation of mission critical systems

Complex software and systems are pervasive in today’s world. In a growing number of fields they come to play a critical role. In order to provide a high assurance level, verification and validation (V&V) should be considered early in the development process. This paper shows how this can be achieved based on a goal-oriented requirements engineering framework which combines complementary semi-formal and formal notations. This allows the analyst to formalize only when and where needed and also preserves optimal communication with stakeholders and developers. For the industrial application of the methodology, a supporting toolbox was developed. It consist of a number of tightly integrated tools for performing V&V tasks at requirements level. This is achieved through the use of (1) a roundtrip mapping between the requirements language and the specific formal languages used in the underlying formal tools (such as SAT or constraint solvers) and (2) graphical views using domain-based representations. This paper will focus on two major and representative tools: the Refinement Checker (about verification) and the Animator (about validation).     

The VALU3S ECSEL project: Verification and validation of automated systems safety and security

Manufacturers of automated systems and their components have been allocating an enormous amount of time and effort in R&D activities, which led to the availability of prototypes demonstrating new capabilities as well as the introduction of such systems to the market within different domains. Manufacturers need to make sure that the systems function in the intended way and according to specifications. This is not a trivial task as system complexity rises dramatically the more integrated and interconnected these systems become with the addition of automated functionality and features to them. This effort translates into an overhead on the V&V (verification and validation) process making it time-consuming and costly. In this paper, we present VALU3S, an ECSEL JU (joint undertaking) project that aims to evaluate the state-of-the-art V&V methods and tools, and design a multi-domain framework to create a clear structure around the components and elements needed to conduct the V&V process. The main expected benefit of the framework is to reduce time and cost needed to verify and validate automated systems with respect to safety, cyber-security, and privacy requirements. This is done through identification and classification of evaluation methods, tools, environments and concepts for V&V of automated systems with respect to the mentioned requirements. VALU3S will provide guidelines to the V&V community including engineers and researchers on how the V&V of automated systems could be improved considering the cost, time and effort of conducting V&V processes. To this end, VALU3S brings together a consortium with partners from 10 different countries, amounting to a mix of 25 industrial partners, 6 leading research institutes, and 10 universities to reach the project goal.     

Combining unit and specification-based testing for meta-model validation and verification

Meta-models play a cornerstone role in Model-Driven Engineering as they are used to define the abstract syntax of modelling languages, and so models and all sorts of model transformations depend on them. However, there are scarce tools and methods supporting their Validation and Verification (V&V), which are essential activities for the proper engineering of meta-models.In order to fill this gap, we propose two complementary meta-model V&V languages. The first one has similar philosophy to the xUnit framework, as it enables the definition of meta-model unit test suites comprising model fragments and assertions on their (in-)correctness. The second one is directed to express and verify expected properties of a meta-model, including domain and design properties, quality criteria and platform-specific requirements.As a proof of concept, we have developed tooling for both languages in the Eclipse platform, and illustrate its use within an example-driven approach for meta-model construction. The expressiveness of our languages is demonstrated by their application to build a library of meta-model quality issues, which has been evaluated over the ATL zoo of meta-models and some OMG specifications. The results show that integrated support for meta-model V&V (as the one we propose here) is urgently needed in meta-modelling environments.     

Software health management: a necessity for safety critical systems

As software and software intensive systems are becoming increasingly ubiquitous, the impact of failures can be tremendous. In some industries such as aerospace, medical devices, or automotive, such failures can cost lives or endanger mission success. Software faults can arise due to the interaction between the software, the hardware, and the operating environment. Unanticipated environmental changes lead to software anomalies that may have significant impact on the overall success of the mission. Latent coding errors can at any time during system operation trigger faults despite the fact that usually a significant effort has been expended in verification and validation (V&V) of the software system. Nevertheless, it is becoming increasingly more apparent that pre-deployment V&V is not enough to guarantee that a complex software system meets all safety, security, and reliability requirements. Software Health Management (SWHM) is a new field that is concerned with the development of tools and technologies to enable automated detection, diagnosis, prediction, and mitigation of adverse events due to software anomalies, while the system is in operation. The prognostic capability of the SWHM to detect and diagnose failures before they happen will yield safer and more dependable systems for the future. This paper addresses the motivation, needs, and requirements of software health management as a new discipline and motivates the need for SWHM in safety critical applications.     

Mitigating Error and Uncertainty in Partitioned Analysis: A Review of Verification,Calibration and Validation Methods for Coupled Simulations

Partitioned analysis involves coupling of constituent models that resolve different scales or physics by allowing them to exchange inputs and outputs in an iterative manner. Through partitioning, simulations of complex physical systems are becoming evermore present in the scientific modeling community, making the Verification and Validation (V&V) of partitioned models to quantifying the predictive capability of their simulations increasingly important. Partitioning presents unique challenges, as well as opportunities, for the V&V community. Verification gains a new level of complexity in partitioned models, as numerical errors can easily be introduced at the coupling interface where non-matching domains and models are integrated together. For validation, partitioned analysis allows the quantification of the uncertainties and errors in constituent models through comparison against separate-effect experiments conducted in independent constituent domains. Such experimental validation is important as uncertainties and errors in the predictions of constituents can be transferred across their interfaces, either compensating for each other or accumulating during iterative coupling operations. This paper reviews published literature on methods for assessing and improving the predictive capability of strongly coupled models of physical and engineering systems with an emphasis on advancements made in the last decade.     

Evaluating the effectiveness of independent verification andvalidation

The complexity of today's software systems mandates a structured approach to development and a verification and validation process that ensure that the right product is built and that it is built right. A V&V process is critical for those high-consequence systems in which a software failure can result in injury or death or where live testing is not feasible. NASA Langley Research Center funded a study to examine the effectiveness of the Army's Software Engineering Evaluation System (SEES). The project led to a study designed to examine the benefits of using SEES as an independent V&V methodology. The study consisted of two independent-development groups. Each was given an identical set of requirements that outlined a solution to a particular problem. The authors asked both groups to design, code, and test their software. The results indicate that IV&V provides a significant value-added component to the software development process     

Blockchain verification and validation: Techniques,challenges, and research directions

As blockchain technology is gaining popularity in industry and society, solutions for Verification and Validation (V&V) of blockchain-based software applications (BC-Apps) have started gaining equal attention. To ensure that BC-Apps are properly developed before deployment, it is paramount to apply systematic V&V to verify their functional and non-functional requirements. While existing research aims at addressing the challenges of engineering BC-Apps by providing testing techniques and tools, blockchain-based software development is still an emerging research discipline, and therefore, best practices and tools for the V&V of BC-Apps are not yet sufficiently developed. In this paper, we provide a comprehensive survey on V&V solutions for BC-Apps. Specifically, using a layered approach, we synthesize V&V tools and techniques addressing different components at various layers of the BC-App stack, as well as across the whole stack. Next, we provide a discussion on the challenges associated with BC-App V&V, and summarize a set of future research directions based on the challenges and gaps identified in existing research work. Our study aims to highlight the importance of BC-App V&V and pave the way for a disciplined, testable, and verifiable BC development.     

Towards software process patterns: An empirical analysis of the behavior of student teams

Traditional software engineering processes are composed of practices defined by roles, activities and artifacts. Software developers have their own understanding of practices and their own ways of implementing them, which could result in variations in software development practices. This paper presents an empirical study based on six teams of five students each, involving three different projects. Their process practices are monitored by time slips based on the effort expended on various process-related activities. This study introduces a new 3-pole graphical representation to represent the process patterns of effort expended on the various discipline activities. The purpose of this study is to quantify activity patterns in the actual process, which in turn demonstrates the variability of process performance. This empirical study provides three examples of patterns based on three empirical axes (engineering, coding and V&V). The idea behind this research is to make developers aware that there is wide variability in the actual process, and that process assessments might be weakly related to actual process activities. This study suggests that in-process monitoring is required to control the process activities. In-process monitoring is likely to provide causal information between the actual process activities and the quality of the implemented components.     

Automatic Generation of Test Oracles—From Pilot Studies to Application

We describe a progression from pilot studies to development and use of domain-specific verification and validation (V&V) automation. Our domain is the testing of an AI planning system that forms a key component of an autonomous spacecraft. We used pilot studies to ascertain opportunities for, and suitability of, automating various analyses whose results would contribute to V&V in our domain. These studies culminated in development of an automatic generator of automated test oracles. This was then applied and extended in the course of testing the spacecraft's AI planning system.Richardson et al. (1992, In Proceedings of the 14th International Conference on Software Engineering, Melbourne, Australia, pp. 105–118), presents motivation for automatic test oracles, and considered the issues and approaches particular to test oracles derived from specifications. Our work, carried through from conception to application, confirms many of their insights. Generalizing from our specific domain, we present some additional insights and recommendations concerning the use of test oracles for V&V of knowledge-based systems.     

A field study of the requirements engineering practice in Australian software industry

Empirical studies have demonstrated that requirements errors introduced during software development are most numerous in the software life-cycle, making software requirements critical determinants of software quality. This article reports an exploratory study which provides insight into industrial practices with respect to requirements engineering (RE). A combination of both qualitative and quantitative data is collected, using semi-structured interviews and a detailed questionnaire from 28 software projects in 16 Australian companies. The contribution of this RE study is threefold: Firstly, it includes a detailed examination of the characteristics of the RE activities involved in the projects. Secondly, it reconstructs the underlying practiced process models. Thirdly, it compares these models to one another and with a number of well-known process models from RE literature to give insight into the gap between RE theory and practice.     

EQUITAS: A tool-chain for functional safety and reliability improvement in automotive systems

To support advanced features such as hybrid engine control, intelligent energy management, and advanced driver assistance systems, automotive embedded systems must use advanced technologies. As a result, systems are becoming distributed and include dozens of Electronic Control Units (ECU). On the one hand, this tendency raises the issue of robustness and reliability, due to the increase in the error ratio with the integration level and the clock frequency. On the other hand, due to a lack of automation, software Validation and Verification (V&V) tends to swallow up 40% to 50% of the total development cost. The ``Enhanced Quality Using Intensive Test Analysis on Simulators'' (EQUITAS¹) project aims (1) to improve reliability and functional safety and (2) to limit the impact of software V&V on embedded systems costs and time-to-market. These two achievements are obtained by (1) developing a continuous tool-chain to automate the V&V process, (2) improving the relevance of the test campaigns by detecting redundant tests using equivalence classes, (3) providing assistance for hardware failure effect analysis (FMEA) and finally (4) assessing the tool-chain under the ISO 26262 requirements.     

复杂工程建模和模拟的验证与确认

综述国内外建模和模拟(Modeling and Simulation,MS)的验证与确认(Verification and Validation,VV)的相关概念、术语、规范、置信度评估方法和应用等方面的发展和研究进展,概括MS的VV中的几个关键问题,构建复杂工程MS的VV的知识指南,为MS的VV技术真正走向应用提供参考.     

A strategy for evaluating a fuzzy case-based construction procurement selection system

System Verification and Validation (V&V) is an essential element in the development and implementation of any computer-based decision tools. The unique concepts of Case-Based Reasoning (CBR), such as the use of mega-knowledge and nearest matching have generated extra challenges to system developers to ensure that the system is built right and the right system is built. However, little attention has been attributed to verifying and validating a CBR system. Recently, a fuzzy CBR prototype known as CaPS has been developed for the selection of appropriate construction procurement systems. To ensure that the procurement system is acceptable to the procurement experts in the construction industry, a series of tests have been conducted with domain experts using real cases (stored in the case base) and projects (as scenarios for retrieval and comparison). This paper reports on the findings of the V&V that have been performed on CaPS. Techniques available for verifying and validating a CBR system are first discussed. The V&V procedures applied to the prototype system are subsequently outlined. The results confirm that the cases stored in CaPS are correct, consistent, and irredundant. More importantly, the solutions generated by CaPS are accurate and innovative, and these are necessary for today's construction projects.     

Verification and validation meet planning and scheduling

A planning and scheduling (P&S) system takes as input a domain model and a goal, and produces a plan of actions to be executed, which will achieve the goal. A P&S system typically also offers plan execution and monitoring engines. Due to the non-deterministic nature of planning problems, it is a challenge to construct correct and reliable P&S systems, including, for example, declarative domain models. Verification and validation (V&V) techniques have been applied to address these issues. Furthermore, V&V systems have been applied to actually perform planning, and conversely, P&S systems have been applied to perform V&V of more traditional software. This article overviews some of the literature on the fruitful interaction between V&V and P&S.     

领域框架的设计

复用技术在软件开发中显得越来越重要 ,但要设计在许多领域都通用的可复用业务组件是很困难的 ,而面向领域的复用是在一个特定应用领域中实现复用。领域工程是软件工程的延伸和扩展 ,它是面向领域的复用。领域框架的设计是领域工程中最主要的工作。本文对其中的关键技术进行了详细剖析 ,并提供了设计领域框架的一些策略     

Verification and validation of knowledge-based systems

Knowledge-based systems (KBSs) are being used in many applications areas where their failures can be costly because of losses in services, property or even life. To ensure their reliability and dependability, it is therefore important that these systems are verified and validated before they are deployed. This paper provides perspectives on issues and problems that impact the verification and validation (V&V) of KBSs. Some of the reasons why V&V of KBSs is difficult are presented. The paper also provides an overview of different techniques and tools that have been developed for performing V&V activities. Finally, some of the research issues that are relevant for future work in this field are discussed     

A framework for computer-aided validation

This paper presents a framework for augmenting independent validation and verification (IV&V) of software systems with computer-based IV&V techniques. The framework allows an IV&V team to capture its own understanding of the application as well as the expected behavior of any proposed system for solving the underlying problem by using an executable system reference model, which uses formal assertions to specify mission- and safety-critical behaviors. The framework uses execution-based model checking to validate the correctness of the assertions and to verify the correctness and adequacy of the system under test.     

Validation of intelligent systems: a critical study and a tool

One of the most important phases in the methodology for the development of intelligent systems is that corresponding to the evaluation of the performance of the implemented product. This process is popularly known as verification and validation (V&V). The majority of tools designed to support the V&V process are preferentially directed at verification in detriment to validation, and limited to an analysis of the internal structures of the system. The authors of this article propose a methodology for the development of a results-oriented validation, and a tool (SHIVA) is presented which facilitates the fulfilment of the tasks included in the methodology, whilst covering quantitative as well as heuristic aspects. The result is an intelligent tool for the validation of intelligent systems.     

Beyond the black box: knowledge overlaps in software outsourcing

The black-box approach - that is, the use of formal project requirements to transfer knowledge about the application problem domain from the client to the vendor organization - has long been the mainstay of outsourced software development. We've studied 209 custom application development projects in 209 global software development organizations. We used the study results to develop detailed guidelines for improving outsourcing practice and a client-vendor knowledge congruence assessment framework. The study's key finding is that effective outsourcing requires knowledge congruence - that is, a good fit in terms of business and technical knowledge across the client-vendor dyad. This uniquely extends the notion of the product/process fit from the manufacturing management arena into the more knowledge-driven domain of software engineering.     

Practical design considerations for successful industrial application of model-based fault detection techniques to aircraft systems

This paper discusses some key factors which may arise for successful application of model-based Fault Detection (FD) techniques to aircraft systems. The paper reports on the results and the lessons learned during flight V&V (Validation & Verification) activities, implementation in the A380 Flight Control Computer (FCC) and A380 flight tests at Airbus (Toulouse, France). The paper does not focus on new theoretical materials, but rather on a number of practical design considerations to provide viable technological solutions and mechanization schemes. The selected case studies are taken from past and on-going research actions between Airbus and the University of Bordeaux (France). One of the presented solutions has received final certification on new generation Airbus A350 aircraft and is flying (first commercial flight: January 15, 2015).