China
Africa
Explore chapters and articles related to this topic
Applications of Formal Methods, Modeling, and Testing Strategies for Safe Software Development
Published in Qamar Mahboob, Enrico Zio, Handbook of RAMS in Railway Systems, 2018
Alessandro Fantechi, Alessio Ferrari, Stefania Gnesi
A formal verification technique that has also recently acquired popularity in industrial applications is model checking (Clarke et al. 1999), an automated technique that, given a finite-state model of a system and a property stated in some appropriate logical formalism (such as temporal logic), checks the validity of this property on the model. Several temporal logics have been defined for expressing interesting properties. A temporal logic is an extension of the classical propositional logic in which the interpretation structure is made of a succession of states at different time instants. An example is the popular computation tree logic (CTL), a branching time temporal logic, whose interpretation structure (also called Kripke structure) is the computation tree that encodes all the computations departing from the initial states.
Principles of DEVS Model Verification for Real-Time Embedded Applications
Published in Katalin Popovici, Pieter J. Mosterman, Real-Time Simulation Technologies, 2017
Hesham Saadawi, Gabriel A. Wainer, Mohammad Moallemi
Embedded systems design must model both the physical system under control and the controller. These models hold more value if they are written in a formalism that can be simulated, such as is the case for DEVS. This allows the designer to simulate the system, change design, and simulate again to reach a correct and optimal design. Formal verification helps verify absence of defects in the system. Once the system is proven to be free of defects, the controller DEVS model, being verified within the complete system, is deployed as the executable controller by running on an embedded DEVS simulator. This eliminates any transformation between the verified model and its implementation, thus avoiding potential defects from creeping into the final implementation because of necessary transformations.
Design of the HyperSurface Networking Aspects
Published in Christos Liaskos, The Internet of Materials, 2020
Dimitrios Kouzapas, Taqua Khairy, Nouman Ashraf, Ileana Papailiou, Anna Philippou, Andreas Pitsillides, Konstantinos Michail, Anastasis Kounoudes
Formal verification is the process of employing formal methods to check whether a system meets its intended specifications (behavior). In the case of the developed HSF-CN, the behavior concerns the correct behavior of the developed algorithms for initialization, routing, and reporting. In contrast to testing and simulative methodologies, formal method techniques perform an exhaustive search of the state space of the model, thereby providing full guarantees of correctness.
Shifting role for human factors in an ‘unmanned’ era
Published in Theoretical Issues in Ergonomics Science, 2018
Karen M. Feigh, Matthew J. Miller, Raunak P. Bhattacharyya, Minyue (Lanssie) Ma, Samantha Krening, Yosef Razin
Formal verification is an analysis technique that is defined by formal methods, which are well-defined mathematical languages and techniques for the specification, modelling and verification of systems. To start, specification properties are mathematical descriptions of the desired system parameters. Essentially specification properties are modelled and verified on how closely they satisfy the specification (Wing 1990). Verification is automatically performed as an automated approach to model checking and covers an exhaustive search in the state-space to see if the properties modelled hold up (Clarke 1999). Formal methods allow researchers to deeply analyse the internals of automation and consider all possible behaviours of a modelled system (Butler 1998). Formal verification has been successful in evaluating human–automation interaction; however, its application has still been limited in this field.
SysML-based compositional verification and safety analysis for safety-critical cyber-physical systems
Published in Connection Science, 2022
Jian Xie, Wenan Tan, Zhibin Yang, Shuming Li, Linquan Xing, Zhiqiu Huang
Complex CPS systems are always hierarchically organised by using component-based architecture. Automatic formal verification techniques such as model-checking can help to analyse the behaviours of such systems. For instance, thanks to a model-checking tool, one can create a model and analyse all of the behaviours of the components in the architecture model. Actually, most of the time, the architecture model is flattened. Nevertheless, doing so, often faces the so-called state-explosion problem. An approach to deal with the state explosion problem is the use of compositional verification which leverages the structure of the system. In these techniques, the verification of a composite system is reduced to the verification of its parts.
Exploration strategies for balancing efficiency and comprehensibility in model checking with ant colony optimization
Published in Journal of Information and Telecommunication, 2022
Tsutomu Kumazawa, Munehiro Takimoto, Yasushi Kambayashi
Formal verification is a mathematical approach to prove or refute correctness of software systems. This article focuses on model checking, which verifies software systems' behavioural aspects automatically (Clarke & Emerson, 1982; Clarke et al., 2018). In model checking, the description of important behaviour of the target system is called a model. The desired property of the system is written as a specification. Model checking assumes that the model and the specification are given by the user. Then it decides whether the model satisfies the specification or not. The problem can be reduced to the exhaustive search problem over the state space constructed from the model and the specification. A model checking tool outputs a violative behaviour, i.e. a counterexample, if it concludes that the model does not satisfy the specification. There are two major research challenges of model checking: State Explosion Problem and the problem of Generating Comprehensible and Short Counterexamples. The state explosion is a problem about verification efficiency. State spaces tend to be huge. For example, the number of states in a concurrent and multiprocessing system often grows exponentially as the number of component processes increases linearly. The state explosion problem claims that huge state spaces make model checking infeasible in practice because the classical exhaustive algorithms deplete computational resources. On the other hand, generating comprehensible counterexamples is a usability problem. A counterexample provides diagnostic information that helps human users understand a specification's violation easily. Therefore, it is more favourable to obtain short counterexamples than to obtain lengthy ones. These problems are in a trade-off relationship. When we want a short counterexample, the exhaustive search is necessary but it suffers from the state explosion. Therefore, we need to pursue a search algorithm such that it achieves the best balance between efficiency and shortness of counterexamples.