China 
Africa 
Explore chapters and articles related to this topic
Models and Tools for Complex Embedded Software and Systems
Published in Luciano Lavagno, Igor L. Markov, Grant Martin, Louis K. Scheffer, Electronic Design Automation for IC System Design, Verification, and Testing, 2017
The use of abstract software models may significantly increase the chances that the design and its implementation are correct, when used at the highest possible level in the development process. Correctness can be mathematically proved by formal reasoning upon the model of the system and its desired properties (provided the model is built on solid mathematical foundations and its properties are expressed by some logic functions). Unfortunately, in many cases, formal model checking is simply impractical, because of the lack of models with a suitable semantics or because of the excessive number of possible states of the system. In this case, the modeling language should at least provide abstractions for the specification of reusable components, so that software modules can be clearly identified with the provided functionality or services.
Component-Based Software Testing Techniques and Test-Case Generation Methods
Published in Umesh Kumar Tiwari, Santosh Kumar, Component-Based Software Engineering, 2020
Umesh Kumar Tiwari, Santosh Kumar
Testing is an attempt to make the software under consideration error free. Identifying and fixing errors in early phases of development is always helpful to minimize overall development costs. Testing software is expensive in terms of cost, effort and time. Testing is one of the critical and crucial phases of the overall development of software. Testing is the fundamental activity to verify the correctness, precision and compatibility of the software at individual level as well as system level. Practitioners have identified that improper testing results in untrustworthy and unreliable products.
Safety Certification of Mixed-Criticality Systems
Published in Hamidreza Ahmadian, Roman Obermaisser, Jon Perez, Distributed Real-Time Architecture for Mixed-Criticality Systems, 2018
I. Martinez, G. Bouwer, F. Chauvel, Ø. Haugen, R. Heinen, G. Klaes, A. Larrucea Ortube, C. F. Nicolas, P. Onaindia, K. Pankhania, J. Perez, A. Vasilevskiy
Verification in Software Engineering is driven by two main approaches: automated testing and formal verification. Testing takes products at the end of development iterations and checks their adherence to specification (e.g., correctness, performance, usability). By contrast, formal verification builds mathematical models of systems and proves their correctness, performance, usability, etc. We review below the main characteristics of the two approaches.
State-based verification of industrial control programs with the use of a digital model
Published in International Journal of Computer Integrated Manufacturing, 2023
Matthias Schamp, El-Houssaine Aghezzaf, Johannes Cottyn
Model checking, which is an automatic verification technique, is mainly applicable to finite-state systems, where all combinations can exhaustively be enumerated: all executions of a given system are examined to answer whether they satisfy a given correctness property. The main tools used for model checking can be classified into three sets of tools (Ovatman et al. 2016): SMV-based tools (NuSMV, CadenceSMV), Timed Automata-based (UPPAAL family, Kronos) and SPIN model checker. Formal model checking requirements are often noted in Linear Temporal Logic (LTL) or Computation Tree Logic (CTL) and used in computer science, but both are not often used in traditional PLC programming (Vardi 2001). The majority of research investigates formal verification techniques using a case-based approach (Sun et al. 2021).
Foundations of mathematics under neuroscience conditions of lateral inhibition and lateral activation
Published in International Journal of Parallel, Emergent and Distributed Systems, 2018
Andrew Schumann, Alexander V. Kuznetsov
In the logical foundations of mathematics there are two approaches in drawing computer-assisted proofs: (i) automated theorem proving (i.e. proving mathematical theorems by computer programs) and (ii) automated proof checking (i.e. using computer programs for checking proofs for correctness). There are many objections for these approaches. For instance, for (i) one the main objections is that these methods do not give new and useful concepts in mathematics in fact, but they present just a long gloomy calculation. For (ii) one of the main objections is that these methods can check just very simple theorems. There are no even insights how to check FLT by computer programs.
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.