China
Africa
Explore chapters and articles related to this topic
Modelling and Simulation of Construction Cyber-Physical Systems
Published in Salah Wesam Alaloul, Cyber-Physical Systems in the Construction Sector, 2022
Syed Saad, Wesam Salah Alaloul, Kumeel Rasheed, Syed Ammad
The SDL is an approach to software development that emerged in the 1990s and has been applied to problems of all sizes, from embedded systems, internet applications through enterprise systems (AlBreiki and Mahmoud 2014). The basic idea behind SDL is that there are seven aspects that must be controlled for a successful software project: quality requirements management (QRM), security requirements management (SRM), performance requirements management (PeRM), reliability requirements management (RRM), maintainability requirements management (MRM), testability requirements management (TRM and portability requirements management (PoRM). This methodology is designed for any kind of system where safety or security concerns exist, such as medical devices or public transportation infrastructure. In that case, you need to create simulations that attempt the impossible and see what happens. One way to create these simulations is by using formal methods like model checking. Formal methods provide the ability to create mathematical descriptions of a system and then use computers to explore the properties of the system. This methodology can also provide increased security if someone’s password is revealed, or an employee leaks their private information.
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.
Formal Methods
Published in Phillip A. Laplante, Requirements Engineering for Software and Systems, 2017
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.