Computer Modeling and Simulation: Increasing Reliability by Disentangling Verification and Validation

Verification and validation (V&V) of computer codes and models used in simulations are two aspects of the scientific practice of high importance that recently have been discussed widely by philosophers of science. While verification is predominantly associated with the correctness of the way a model is represented by a computer code or algorithm, validation more often refers to the model’s relation to the real world and its intended use. Because complex simulations are generally opaque to a practitioner, the Duhem problem can arise with verification and validation due to their entanglement; such an entanglement makes it impossible to distinguish whether a coding error or the model’s general inadequacy to its target should be blamed in the case of a failure. I argue that a clear distinction between computer modeling and simulation has to be made to disentangle verification and validation. Drawing on that distinction, I suggest to associate modeling with verification and simulation, which shares common epistemic strategies with experimentation, with validation. To explain the reasons for their entanglement in practice, I propose a Weberian ideal–typical model of modeling and simulation as roles in practice. I examine an approach to mitigate the Duhem problem for verification and validation that is generally applicable in practice and is based on differences in epistemic strategies and scopes. Based on this analysis, I suggest two strategies to increase the reliability of simulation results, namely, avoiding alterations of verified models at the validation stage as well as performing simulations of the same target system using two or more different models. In response to Winsberg’s claim that verification and validation are entangled I argue that deploying the methodology proposed in this work it is possible to mitigate inseparability of V&V in many if not all domains where modeling and simulation are used.

     

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.     

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.     

A framework for verification,validation, and refinement of knowledge bases: The VVR system

Verification and validation (V&V) of Knowledge Bases (KBs) are two sides of the same coin: one is intended to assure the structural correctness of the KB, while the other is intended to assure the functional correctness of the domain model embodied in the KB. Knowledge base refinement aims to appropriately revise the KB if a structural or functional error is detected during the V&V process. This paper presents a uniform framework for verification, validation and refinement of KBs represented as sets of production rules, called the VVR system. It incorporates a contradiction-tolerant truth maintenance system (CTMS) for performing both verification and validation analyses, and some simple explanation-based learning techniques for guiding the refinement process. Verification analysis consists of detecting and correcting the main types of structural anomalies: circular rules, redundant rules, inconsistent rules, and inconsistent data, and checks the KB for completeness and violated semantic constraints. In terms of validation, given a set of test cases, the VVR system is capable of detecting and correcting functional errors caused by overgeneralization and/or overspecialization of the KB. If the set of test cases is not available, the VVR system can generate synthetic test cases intended to help the user evaluate KBS performance. © 1994 John Wiley & Sons, Inc.     

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.     

A distributed approach to verification and validation of electronic structure simulation data using ESTEST

We present a Verification and Validation (V&V) approach for electronic structure computations based on a network of distributed servers running the ESTEST (Electronic Structure TEST) software. This network-based infrastructure enables remote verification, validation, comparison and sharing of electronic structure data obtained with different simulation codes. The implementation and configuration of the distributed framework is described. ESTEST features are enhanced by server communication and data sharing, minimizing the duplication of effort by separate research groups. We discuss challenges that arise from the use of a distributed network of ESTEST servers and outline possible solutions. A community web portal called ESTEST Discovery is introduced for the purpose of facilitating the collection and annotation of contents from multiple ESTEST servers. We describe examples of use of the framework using two currently running servers at the University of California Davis and at the Centre Européen de Calcul Atomique et Moléculaire (CECAM).     

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.     

A new specification-based qualitative metric for simulation model validity

Informal validation techniques such as simulation are extensively used in the development of embedded systems. Formal approaches such as model-checking and testing are important means to carry out Verification and Validation (V&V) activities. Model-checking consists in exploring all possible behaviors of a model in order to perform a qualitative and quantitative analysis. However, this method remains of limited use as it runs into the problem of combinatorial explosion. Testing and model-checking do not take into account the context of use objectives of the model. Simulation overcomes these problems but it is not exhaustive. Submitted to simulation scenarios which are an operational formulation of the V&V activity considered, simulation consists in exploring a subset of the state space of the model. This paper proposes a formal approach to assess simulation scenarios. The formal specification of a model and the simulation scenarios applied to that model serve to compute the effective evolutions taken by the simulation. It is then possible to check whether a simulation fulfills its intended purpose. To illustrate this approach, the application study of an intelligent cruise controller is presented. The main contribution of this paper is that combining simulation objectives and formal methods leads to define a qualitative metric for a simulation evaluation without running a simulation.     

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.     

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.     

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.     

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

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

The European ADDSAFE project: Industrial and academic efforts towards advanced fault diagnosis

In this article a high-fidelity aircraft benchmark, developed by Airbus for advanced flight control related studies, is presented in relation to its evolution towards advanced fault diagnosis within a European 7th Framework Program project entitled “Advanced Fault Diagnosis for Sustainable Flight Guidance and Control (ADDSAFE)”. This European project was established to study and facilitate the transfer of model-based fault detection and diagnosis methods from Academia to Industry. The importance of the project arose on the one hand, due to the representativeness of the benchmark, and on the other hand, the industrial benchmarking and validation of the developed designs. The results presented in this article represent a quantitative measure of the success of the project since five of the developed designs were successfully validated in Airbus Verification and Validation (V&V) set-ups, and are currently undergoing further tests towards a possible real aircraft implementation.     

The need for verifiable visualization

Visualization is often employed as part of the simulation science pipeline-it's the window through which scientists examine their data for deriving new science, and the lens used to view modeling and discretization interactions within their simulations. We advocate that as a component of the simulation science pipeline, visualization must be explicitly considered as part of the validation and verification (V&V) process. In this article, the authors define V&V in the context of computational science, discuss the role of V&V in the scientific process, and present arguments for the need for verifiable visualization.     

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.     

Advanced and efficient execution trace management for executable domain-specific modeling languages

Executable Domain-Specific Modeling Languages (xDSMLs) enable the application of early dynamic verification and validation (V&V) techniques for behavioral models. At the core of such techniques, execution traces are used to represent the evolution of models during their execution. In order to construct execution traces for any xDSML, generic trace metamodels can be used. Yet, regarding trace manipulations, generic trace metamodels lack efficiency in time because of their sequential structure, efficiency in memory because they capture superfluous data, and usability because of their conceptual gap with the considered xDSML. Our contribution is a novel generative approach that defines a multidimensional and domain-specific trace metamodel enabling the construction and manipulation of execution traces for models conforming to a given xDSML. Efficiency in time is improved by providing a variety of navigation paths within traces, while usability and memory are improved by narrowing the scope of trace metamodels to fit the considered xDSML. We evaluated our approach by generating a trace metamodel for fUML and using it for semantic differencing, which is an important V&V technique in the realm of model evolution. Results show a significant performance improvement and simplification of the semantic differencing rules as compared to the usage of a generic trace metamodel.

     

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).     

Approximate declarative semantics for rule base anomalies

Despite the fact that there has been a surge of publications in verification and validation of knowledge-based systems and expert systems in the past decade, there are still gaps in the study of verification and validation (V&V) of expert systems, not the least of which is the lack of appropriate semantics for expert system programming languages. Without a semantics, it is hard to formally define and analyze knowledge base anomalies such as inconsistency and redundancy, and it is hard to assess the effectiveness of V&V tools, methods and techniques that have been developed or proposed. In this paper, we develop an approximate declarative semantics for rule-based knowledge bases and provide a formal definition and analysis of knowledge base inconsistency, redundancy, circularity and incompleteness in terms of theories in the first order predicate logic. In the paper, we offer classifications of commonly found cases of inconsistency, redundancy, circularity and incompleteness. Finally, general guidelines on how to remedy knowledge base anomalies are given.     

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.