Search

Formal methods (FMs) have been cited as a viable methodology for developing high-quality software. However, the steep learning curve in efficiently using the underlying discrete mathematics and logic has hindered FMs' adoption, leading to a decline in their initial interest in the 1980s. Traditionally, technical approaches have been pursued to address the FMs challenge. Having taken cognisance of a similar pre-4IR decline in AI, the researcher views FMs as technology and considers solutions at intersections of 4IR-5IR technology adoption, leveraged by the support of governors, termed leadership-management in this work. Following a qualitative research choice, scholarly literature is reviewed, and sets of qualitative propositions are defined to develop a conceptual framework for a 4IR-5IR leadership-management adoption of FMs. Aspects that emerged and are incorporated into the framework are cross-functional and executive levels of leadership, transformative, adaptive, and servant leadership styles, using FM tools that embed a high level of user experience, and 4IR technologies, augmented with 5IR human aspects. The framework is hoped to motivate a company's leadership to contribute to technology and technical ICT-based decision-making increasingly. Future work in this area would involve securing input from practitioners and exercising the framework in an industrial setting. [ABSTRACT FROM AUTHOR]

This paper reports on the development and validation of a formal model for an automotive adaptive exterior lights system (ELS) with multiple variants in Alloy 6, which is the most recent version of the Alloy lightweight formal specification language that supports mutable relations and temporal logic. We explore different strategies to address variability, one in pure Alloy and another through an annotative language extension. We then show how Alloy and its Analyzer can be used to validate systems of this nature, namely by checking that the reference scenarios are admissible, and to automatically verify whether the established requirements hold. A prototype was developed to translate the provided validation sequences into Alloy and back to further automate the validation process. The resulting ELS model was validated against the provided validation sequences and verified for most of requirements for all variants. [ABSTRACT FROM AUTHOR]

Team formation in an environment where some relevant parameters are not known in advance is a challenging problem. Communicating automata and distributed algorithms have been used to describe protocols for team formation. A high‐level specification provides a mathematical description of a protocol or a program. TLA +$$ {}^{+} $$ is a formal specification language designed to provide high‐level specifications of concurrent and distributed systems. The associated model checker known as TLC is capable of model checking the TLA +$$ {}^{+} $$ specifications. Recently, formal specification of a team formation protocol is given using TLA +$$ {}^{+} $$ when there is a single initiator (an agent or a robot) that initiates the team formation. Using TLA +$$ {}^{+} $$, we examine the formal specification for the multiple initiator situation and demonstrate that a composition technique can yield a single monolithic specification for the multiple initiator situation from the single initiator situation specification. We have used models of varying sizes, and the TLC model checker has confirmed that the protocol's specifications meet certain desired characteristics in each case. [ABSTRACT FROM AUTHOR]

The reference point for developing any artefact is its specification; to develop software formally, a formal specification is required. For sequential programs, pre and post conditions (together with abstract objects) suffice; rely and guarantee conditions extend the scope of formal development approaches to tackle concurrency. In addition, real-time systems need ways of both requiring progress and relating that progress to some notion of time. This paper extends rely-guarantee ideas to cope with specifications of—and assumptions about—real-time schedulers. Furthermore it shows how the approach helps identify and specify fault-tolerance aspects of such schedulers by systematically challenging the assumptions. [ABSTRACT FROM AUTHOR]

In recent years, the field of security requirements specification by formal methods has changed radically. The security requirement specification is now one of the widely recognized as well as actively pursued research challenges in both requirement engineering and security engineering communities. In this paper, we focus on the research metadata to find the state of the art in the field of security requirements specification using the formal approach. In order, a review was taken up to perform metadata, obtained from frequently used databases. In total, 200 publications were retrieved; out of which 110 were found to be relevant to our research questions. The results of metadata provided an insight into the main contributions of the field, research gaps, and challenges, which motivated the discussion for important research direction in the future. [ABSTRACT FROM AUTHOR]

At present, formal methods significantly facilitate the specification and verification of security requirements in requirement engineering, which can reduce requirement errors in the early stage of system development. Extracting formal specifications from security requirements and then evaluating the quality of the requirements are regarded as a promising solution to ensure software quality. Propositional projection temporal logic (PPTL) with a strong mathematical basis and full regular expressiveness is a suitable language for formal specifications. Inspired by natural language processing and text mining techniques, this paper designs and implements a tool, namely, NL2PPTL, to generate formal coarse‐grained and fine‐grained specifications in terms of PPTL formulas automatically. In specific, the grammatical production rules are defined to construct the syntax tree, and then, the formula is obtained by post‐order traversal of the tree. The satisfiability of the PPTL specifications can be checked utilizing PPTLSAT. In addition, the state transformation model is constructed from fine‐grained specifications, so as to discover scope conflicts and verify the security properties of the requirement case. [ABSTRACT FROM AUTHOR]

Real-time audio/video transmission through Internet media is an important part of communication. Due to bandwidth limitations and a noisy environment, delivery of multimedia content to a remote location is not 100% guaranteed. These limitations are the basic cause of missing packets which affect the Quality of Service (QoS). A protocol for the recovery of lost packets is described in [Maxemchuk, Nicholas F., K. Padmanabhan, and S. Lo. “A cooperative packet recovery protocol for multicast video.” Network Protocols, 1997. Proc. of 1997 International Conference on. IEEE]. This protocol claims significant improvement in QoS. We formally specify the protocol in a network of timed automata. By model-checking (A mathematical technique), we find that packet recovery is not always there. In this article, We report such scenarios of malfunctioning in the protocol when the size of multimedia contents is known (e.g., live video/audio broadcasting) and middle-level servers have different rates of data sending and receiving. We formulate the effect of inter-packet delay and transmission speed difference on a buffer.

Attestation is one of the most critical mechanisms in confidential computing (CC). We present a holistic verification approach enabling comprehensive and rigorous security analysis of architecturally-defined attestation mechanisms in CC. Specifically, we analyze two prominent next-generation hardware-based Trusted Execution Environments (TEEs), namely Arm Confidential Compute Architecture (CCA) and Intel Trust Domain Extensions (TDX). For both of these solutions, we provide a comprehensive specification of all phases of the attestation mechanism, namely provisioning, initialization, and attestation protocol. We demonstrate that including the initialization phase in the formal model leads to a violation of integrity, freshness, and secrecy properties for Intel’s claimed trusted computing base (TCB), which could not be captured by considering the attestation protocol alone in the related work. We open-source our artifacts. Other researchers, including a team from Intel, are adopting our artifacts for further analysis.

Formal methods (FMs) have been cited as a viable methodology for developing high-quality software. However, the steep learning curve in efficiently using the underlying discrete mathematics and logic has hindered FMs’ adoption, leading to a decline in their initial interest in the 1980s. Traditionally, technical approaches have been pursued to address the FMs challenge. Having taken cognisance of a similar pre-4IR decline in AI, the researcher views FMs as technology and considers solutions at intersections of 4IR-5IR technology adoption, leveraged by the support of governors, termed leadership-management in this work. Following a qualitative research choice, scholarly literature is reviewed, and sets of qualitative propositions are defined to develop a conceptual framework for a 4IR-5IR leadership-management adoption of FMs. Aspects that emerged and are incorporated into the framework are cross-functional and executive levels of leadership, transformative, adaptive, and servant leadership styles, using FM tools that embed a high level of user experience, and 4IR technologies, augmented with 5IR human aspects. The framework is hoped to motivate a company’s leadership to contribute to technology and technical ICT-based decision-making increasingly. Future work in this area would involve securing input from practitioners and exercising the framework in an industrial setting.

The Unified Modeling Language (UML) is a standard for modeling dynamic systems. UML behavioral state machines are used for modeling the dynamic behavior of object-oriented designs. The UML specification, maintained by the Object Management Group (OMG), is documented in natural language (in contrast to formal language). The inherent ambiguity of natural languages may introduce inconsistencies in the resulting statemachine model. Formalizing UML state machine specification aims at solving the ambiguity problem and at providing a uniform view to software designers and developers. Such a formalization also aims at providing a foundation for automatic verification of UML state machine models, which can help to find software design vulnerabilities at an early stage and reduce the development cost. We provide here a comprehensive survey of existing work from 1997 to 2021 related to formalizing UML state machine semantics for the purpose of conducting model checking at the design stage. [ABSTRACT FROM AUTHOR]

Summary: The automation of programming, which lies at the intersection of software engineering and artificial intelligence, enables machines to automatically generate programs that satisfy given requirements. In the context of B formal design modeling, one of the challenges is the refactoring of substitutions in design specifications, which often uses state transitions to describe how program or system statuses change during execution. This paper proposes a condition and substitution refactoring algorithm for the B formal specification language. The aim of the work is to automatically derive B operational predicates based on given transitions. The work has been extremely useful to machine‐driven formal design model repair as well as automated design specification generation. Given a set of state transitions, common relations of their state variables can be discovered and clustered into a number of classes. These relations can be further used to synthesize substitutions that derive new states from existing states. To restrict application domains of the synthesized substitutions, conditions that guard these substitutions are generated using first‐order logic. We have implemented the proposed algorithm as an extension to the ProB model checker. Experiments were conducted based on the B model public dataset. The evaluation results demonstrated that our solution is able to synthesize conditions and substitutions for various sets of state transitions in a wide range of B models. [ABSTRACT FROM AUTHOR]

Abstract Formal methods are proven techniques that provide a rigorous mathematical basis to software development. In particular, they allow the quality of development to be effectively improved by making accurate and explicit modelling, so that anomalies like ambiguities and incompleteness are identified in the early phases of the software development process. Semi‐formal UML models and formal Timed Automata models are used to design a telerehabilitation system through a practical approach based on abstraction and refinement. The formal verification of expected properties of the system is performed by the Uppaal tool. The motivation of this work is threefold: (i) showing the usefulness of formal methods to satisfy the validation needs of a medical telerehabilitation system; (ii) demonstrating our approach of system analysis through refinements to guide the development of a complex system; and (iii) highlighting, from a real‐life experience, the usefulness of models to involve the stakeholders all along the design of a system, from requirements to detailed specifications.

The European Railway Agency has formulated assumptions for a target model of rail transport. Its important premise is digitalization to support the communication and transport services that the railways will make available to the public in the future. Part of the digitalization process is the digital description of the railway infrastructure in a formalized form to allow algorithmic processing. The formal description of infrastructure is not a new issue. However, attempts made so far have not resulted in a permanent definition of a generally accessible formalism allowing for a coherent representation of the physical railway infrastructure in a digital form. This paper presents the results of work carried out within the research project Digital Railway-The Digital Twin of the ETCS Application-Virtual Prototyping and Simulation of Operational Scenarios.

In this paper, we aim to contribute to the knowledge about how imperative C functions can be transformed to Maude functional and system modules respectively. Maude is a formal specification language characterized by simplicity, expressivity and good performance. It is a multi-paradigm meta-language based on rewriting logic and equational theories used to specify, simulate and formally verify concurrent and distributed systems. Maude has been used to define the operational semantics of many programming and specification languages. In particular, the addition of this paper is to close the gap between a subset of the C standard language and Maude relying on a transformational approach.

Abstract Software faults are costly to find and remove from programs. It is better to avoid inserting the faults in the first place. The authors identify requirements‐related faults that can arise during the transformation of formal specifications into programs, analyse each to discover its causes, and propose corresponding fault prevention methods. The approach works by analysing a specification, decomposing it into specification fragments with different levels like components, determining the correct implementation order among the components, and enabling automated code generation for the components and other low‐level specification fragments. The approach seeks to reduce the faults in programs significantly by guiding programmers to work effectively and productively. The authors evaluate the approach's performance experimentally and compare it to the performance of a fault‐prevention method with industry applications.

Formal methods are proven techniques that provide a rigorous mathematical basis to software development. In particular, they allow the quality of development to be effectively improved by making accurate and explicit modelling, so that anomalies like ambiguities and incompleteness are identified in the early phases of the software development process. Semi‐formal UML models and formal Timed Automata models are used to design a telerehabilitation system through a practical approach based on abstraction and refinement. The formal verification of expected properties of the system is performed by the Uppaal tool. The motivation of this work is threefold: (i) showing the usefulness of formal methods to satisfy the validation needs of a medical telerehabilitation system; (ii) demonstrating our approach of system analysis through refinements to guide the development of a complex system; and (iii) highlighting, from a real‐life experience, the usefulness of models to involve the stakeholders all along the design of a system, from requirements to detailed specifications. [ABSTRACT FROM AUTHOR]

Abstract The state space explosion restricts the error detection of concurrent software. The abstraction can provide a solution to avoid state space explosion, but it is easy to ignore important details, resulting in inaccurate detection results. This paper proposes a methodology of fine‐coarse‐grained automatic modelling for Java source programs. By the principle that the execution details of property‐unchecked, non‐interactive, and unrelated statements do not affect the model checking results, we model coarse‐grained model fragments for such statements, while fine‐grained model fragments for property‐checked, interactive, and related statements. Our method reduces the model and state space and ensures the error detection of the source program based on model checking. Moreover, we prove the equivalence of the fine‐grained model, the coarse‐grained model, and the program. Finally, this paper gives an experiment to verify the effectiveness of the proposed method.

In an article published in IEEE Access in 2020, researchers present an approach to using TLA+ for the formal verification of whether a network of SDN (Software-Defined Networking) switches implements the filtering rules of a given monolithic firewall. The distributed as well as monolithic firewalls are specified with TLA+. It is shown that the correctness of the former with respect to the latter can be verified automatically by using the TLC model checker. The main contributions of this paper are the following improvements of that approach. Firstly, by specifying switches without using any variables, the time needed for the model checking is reduced significantly. For example, the verification of the same networks takes a few seconds with the new approach and does not end after several hours with the previous one. Secondly, the following problem is solved. With the latter, if a monolithic firewall allows a packet to pass through, all the paths in the distributed firewall which the packet is routed on must allow the same. Otherwise, the model checker proclaims the distributed firewall to be in error. We present an additional approach to the verification, which gives a positive answer if at least one of the paths allows the packet to pass through.

Software faults are costly to find and remove from programs. It is better to avoid inserting the faults in the first place. The authors identify requirements‐related faults that can arise during the transformation of formal specifications into programs, analyse each to discover its causes, and propose corresponding fault prevention methods. The approach works by analysing a specification, decomposing it into specification fragments with different levels like components, determining the correct implementation order among the components, and enabling automated code generation for the components and other low‐level specification fragments. The approach seeks to reduce the faults in programs significantly by guiding programmers to work effectively and productively. The authors evaluate the approach's performance experimentally and compare it to the performance of a fault‐prevention method with industry applications. [ABSTRACT FROM AUTHOR]

The European Railway Agency has formulated assumptions for a target model of rail transport. Its important premise is digitalization to support the communication and transport services that the railways will make available to the public in the future. Part of the digitalization process is the digital description of the railway infrastructure in a formalized form to allow algorithmic processing. The formal description of infrastructure is not a new issue. However, attempts made so far have not resulted in a permanent definition of a generally accessible formalism allowing for a coherent representation of the physical railway infrastructure in a digital form. This paper presents the results of work carried out within the research project Digital Railway-The Digital Twin of the ETCS Application-Virtual Prototyping and Simulation of Operational Scenarios. [ABSTRACT FROM AUTHOR]

Autonomous driving systems are crucial complicated cyber–physical systems that combine physical environment awareness with cognitive computing. Deep reinforcement learning is currently commonly used in the decision-making of such systems. However, black-box-based deep reinforcement learning systems do not guarantee system safety and the interpretability of the reward-function settings in the face of complex environments and the influence of uncontrolled uncertainties. Therefore, a formal security reinforcement learning method is proposed. First, we propose an environmental modeling approach based on the influence of nondeterministic environmental factors, which enables the precise quantification of environmental issues. Second, we use the environment model to formalize the reward machine's structure, which is used to guide the reward-function setting in reinforcement learning. Third, we generate a control barrier function to ensure a safer state behavior policy for reinforcement learning. Finally, we verify the method's effectiveness in intelligent driving using overtaking and lane-changing scenarios. [ABSTRACT FROM AUTHOR]

The state space explosion restricts the error detection of concurrent software. The abstraction can provide a solution to avoid state space explosion, but it is easy to ignore important details, resulting in inaccurate detection results. This paper proposes a methodology of fine‐coarse‐grained automatic modelling for Java source programs. By the principle that the execution details of property‐unchecked, non‐interactive, and unrelated statements do not affect the model checking results, we model coarse‐grained model fragments for such statements, while fine‐grained model fragments for property‐checked, interactive, and related statements. Our method reduces the model and state space and ensures the error detection of the source program based on model checking. Moreover, we prove the equivalence of the fine‐grained model, the coarse‐grained model, and the program. Finally, this paper gives an experiment to verify the effectiveness of the proposed method. [ABSTRACT FROM AUTHOR]

The product line approach enables the rapid building of software products by reusing core assets. How to manage the commonality and variability of product family is the core problem of product line engineering. The feature modeling approach is one of the main approaches to solve this problem. However, this approach does not define the internal functions of features. Some researchers use formal descriptions to define the function of features, but they do not consider the connection between feature specification and feature model. These product family modeling approaches result in product family models that suffer from inconsistent descriptions, which are difficult to resolve manually. To this end, this paper proposes a computer-aided approach to construct an internally consistent product family model. The method performs an inconsistency check during the formalization of each feature in the given initial feature model, pushing the evolution of the feature model and feature specification. The creation and evolution of feature models are achieved through a template-based feature modeling approach. The method is implemented by means of templates, each of which contains two parts of knowledge: the elements required for a class of feature model, and a way to convert the given elements into a formal description. An inconsistency check is achieved through a rule-based detection approach. Each rule contains two parts: a class of conditions that the feature model and the feature specification satisfy, and the actions to resolve inconsistencies once the conditions are satisfied. We have developed a tool. The tool guides the user to build an internally consistent product family model that contains the feature model and feature specifications. Experiments have shown that our approach can provide effective automation support for the process of formal product family modeling. [ABSTRACT FROM AUTHOR]

Programmable Logic Controllers are industrial digital computers used as automation controllers in manufacturing processes. The Ladder language is a programming language used to develop software for such controllers. In this work, we consider the description of the expected behaviour of a Ladder program under the form of a timing chart, describing a scenario of execution. Our aim is to prove that the given Ladder program conforms to the expected temporal behaviour given by such a timing chart. Our approach amounts to translating the Ladder code, together with the timing chart, into a program for the Why3 environment for deductive program verification. The verification proceeds with the generation of verification conditions: mathematical formulas to be checked valid using automated theorem provers. The ultimate goal is twofold. On the one hand, by obtaining a complete proof, one verifies the conformity of the Ladder code with respect to the timing chart with a high degree of confidence. On the other hand, in the case the proof is not fully completed, one obtains a counterexample, illustrating a possible execution scenario of the Ladder code which does not conform to the timing chart. [ABSTRACT FROM AUTHOR]

This paper proposes an approach to the specification and model checking of a large, important class of distributed algorithms called control algorithms (CAs), which are superimposed on underlying distributed systems (UDSs). The approach is based on rewriting logic by moving from its object level to the meta-level. We introduce the idea of specifying CAs as meta-programs that take the specifications of UDSs and automatically generate the specifications of the UDSs on which the CAs are superimposed (UDS-CAs). Due to many options, such as network topologies, even fixing the number of each kind of entities, such as mobile support stations (MSSs) and mobile hosts (MHs) in a mobile checkpointing algorithm, there are many instances of a UDS. To address the problem, we generate all possible initial states of a UDS for a fixed number of each kind of entities such that some constraints, such as MSSs strongly connected with a wired network, are fulfilled and conduct model checking for each of the initial states. We demonstrate the usefulness by reporting on a case study where a counterexample is found for some specific initial states but not for the other initial states, detecting a subtle flaw lurking in a mobile checkpointing algorithm. [ABSTRACT FROM AUTHOR]