China
Africa
Explore chapters and articles related to this topic
DO-333 and Formal Methods
Published in Leanna Rierson, Developing Safety-Critical Software, 2017
Formal methods refers to the use of techniques from logic and discrete mathematics in the specification, design, and construction of computer systems (both hardware and software) and relies on a discipline that requires the explicit enumeration of all assumptions and reasoning steps. Each reasoning step must be an instance of a relatively small number of allowed rules of inference. In essence, system verification is reduced to a calculation that can be checked by a machine. In principle, these techniques can produce error-free design; however, this requires a complete verification from the requirements down to the implementation, which is rarely done in practice. Thus, formal methods is the applied mathematics of computer systems engineering. It serves a similar role in computer design as Computational Fluid Dynamics (CFD) plays in aeronautical design, providing a means of calculating and hence predicting what the behavior of a digital system will be prior to its implementation.
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
In general, different techniques are used to reason about these models and gain confidence in the correctness of a design. Informal methods usually rely on extensive testing of the systems based on system specification. These techniques can reveal errors but cannot prove nonexistence of errors. Instead, formal techniques can prove the correctness of a design. Unfortunately, formal approaches are usually constrained in their applications, as they do not scale up well and they require the user to have expert knowledge in applying formal techniques. Another drawback of applying formal techniques is that they must be applied to an abstract model of the target system to be practical. However, in doing so, what is being verified is not the final executable system. Even if the abstract model is correct, there is a risk that some errors creep into the implementation through the manual process of implementing specifications into executable code [1].
Formal Methods
Published in Phillip A. Laplante, Mohamad H. Kassab, Requirements Engineering for Software and Systems, 2022
Phillip A. Laplante, Mohamad H. Kassab
Formal methods are used primarily for systems specification and verification. Users of UML 2.5 could rightly be said to be employing formal methods, but only in the specification sense. The languages B, VDM, Z, Larch, CSP, and statecharts, and various temporal logics are typically used for systems specification. And while the clarity and precision of formal systems specification are strong endorsements for these, it is through verification methods that formal methods really show their power. Formal methods can be used for two kinds of verification: theorem proving (for program proving) and model checking (for requirements validation). We will focus on the former.
Automated simulation and verification of process models discovered by process mining
Published in Automatika, 2020
Ivona Zakarija, Frano Škopljanac-Mačina, Bruno Blašković
Model checking is a formal method for software and hardware system verification. Its goal is to check whether a model of a system satisfies given specification. We will use the Spin model checker that was developed at the Bell Labs by G.J. Holzman [42]. Spin model checker is primarily used for formal verification of distributed systems, such as communication protocols. Spin can run random simulations of the process model or perform a verification of the process model by exploring all the possible execution paths. To formally describe process models, we use Spin's Promela language (Process meta language). Some basic elements of the Promela syntax are similar to the standard C language, but with a different semantics that implicitly enables non-determinism and statement blocking in the execution of the program code. For example, the order of execution in the conditional if–then-else statement is not predetermined – Spin will non-deterministically execute one of the branches that are not blocked. Specifications that are used to check model correctness are invariants – statements that must be true during the entire execution run. They can be defined as assert statements or more formally as Linear temporal logic (LTL) formulae [16,42]. LTL is a modal logic that uses temporal operators, e.g. finally and globally in addition to common logical operators, e.g. negation, conjunction, disjunction and logical implication.
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.
DevFemOps: enhancing maintainability based on microservices using formal engineering methods
Published in Connection Science, 2022
Tetsuo Fukuzaki, Shaoying Liu, Michael Butler
In software development, formal methods are one of the techniques to improve the quality of software development. Formal methods consist of formal specification descriptions and formal proofs. Formal specification descriptions use set theory and logic to describe software specifications, so that functional requirements can be described without ambiguity. First, we can write a formal specification with a high level of abstraction, and then increase the explicitness of the specification through a process of refinement. Formal proofs are used to guarantee that there are no contradictions in the specifications at a certain stage, and that the refinement process has been carried out correctly.