Modeling, verifying, and validating are essential steps in order to build systems and software that do what designers expect. If formal verification, and especially model-checking, is a popular ...method for proving the correctness of properties, its efficiency depends on the accuracy of the used models and the quality of abstractions. As a consequence, applying verification techniques on large-scale complex software like video games is hard without strong assumptions and simplifications. Simulation models are generally more accurate than verification models, but it is often harder to verify them. Combined formalisms that take the benefits of both model-checking and discrete-event simulation represent a good deal between both of these families, although strong engineering expertise remains necessary to define the relevant tests and scenarios. This paper proposes an approach to build this kind of formalism through the example of DEv-PROMELA, which is built by combining Discrete-event System Specification formalism and PROMELA language. Then, it shows how combined formalisms can be used for modeling, verifying, and validating complex software like video games by using both formal-based and simulation-based verification and validation.
IoT environments are forecasted to grow exponentially in the coming years thanks to the recent advances in both edge computing and artificial intelligence. In this paper, a model of remote computing ...scheme is presented, where three layers of computing nodes are put in place in order to optimize the computing and forwarding tasks. In this sense, a generic layout has been designed so as to easily achieve communications among the diverse layers by means of simple arithmetic operations, which may result in saving resources in all nodes involved. Traffic forwarding is undertaken by means of forwarding tables within network devices, which need to be searched upon in order to find the proper destination, and that process may be resource-consuming as the number of entries in such tables grow. However, the arithmetic framework proposed may speed up the traffic forwarding decisions as relaying on integer divisions and modular arithmetic, which may result more straightforward. Furthermore, two diverse approaches have been proposed to formally describe such a design by means of coding with Spin/Promela, or otherwise, by using an algebraic approach with Algebra of Communicating Processes (ACP), resulting in a explosion state for the former and a specified and verified model in the latter.
Summary
In existing computer systems, file systems are indispensable for organizing user data and system codes. However, several studies have reported certain file system errors that cause ...significant data loss or system crashes. Most of these errors are due to external failures, such as an unexpected power outage. However, comprehensively evaluating file system robustness to detect these errors is challenging. The various types of file systems use different data structures and algorithms for various applications. Moreover, file system errors may be triggered by an unpredictable external condition. In addition, a file system works in an operating system's kernel layer as a passive module and runs in a multi‐thread mode, which makes file system testing time‐intensive. Furthermore, the large number of states in file systems leads to greedy checking, which results in a state explosion. In this study, we comprehensively evaluated the robustness expected in multiple properties of file systems using a model checking approach. The evaluation covered the majority of the mainstream file system types and included both single‐thread and multi‐thread modes. We developed Promela models that ed the real file systems and subsequently checked them using a SPIN model checker. Our model was optimized to avoid state explosion during model checking. Using the model checking, we successfully detected corner‐case errors during an unexpected power outage. By analysing counterexamples generated by model checking, we determined an improved file system model capable of preventing errors in most mainstream file system types. Finally, we rechecked the improved file system model and verified the absence of all critical errors.
In this study, we comprehensively evaluated the robustness of the mainstream file system types, expected in multiple properties and both single‐thread and multi‐thread modes. We developed Promela models that ed the real file systems, optimized them to avoid state explosion, checked them using a SPIN model checker, and detected corner‐case errors in the condition of an unexpected power outage. By analysing counterexamples, we developed an improved file system model that verified the absence of all critical errors.
In this article, we focus on the usage of MQTT (Message Queuing Telemetry Transport) within Connected Vehicles (CVs). Indeed, in the original version of MQTT protocol, the broker is responsible ..."only" for sending received data to subscribers; abstracting then the underlying mechanism of data exchange. However, within CVs context, subscribers (i.e., the processing infrastructure) may be overloaded with irrelevant data, in particular when the requirement is real or near real-time processing. To overcome this issue, we propose MQTT-CV; a new variant of MQTT protocol, in which the broker is able to perform local processing in order to reduce the workload at the infrastructure; i.e., filtering data before sending them. In this article, we first validate formally the correctness of MQTT-CV protocol (i.e., the three components of the proposed protocol are correctly interacting), through the use of Promela language and its system verification tool; the model checker SPIN. Secondly, using real-world data provided by our car manufacturer partner, we have conducted real implementation and experiments. The obtained results show the effectiveness of our approach in term of data workload reduction at the processing infrastructure. The mean improvement, besides the fact that it is dependent of the target application, was in general about 10 times less in comparison to native MQTT protocol.
Edge computing applications leverage advances in edge computing along with the latest trends of convolutional neural networks in order to achieve ultra-low latency, high-speed processing, low-power ...consumptions scenarios, which are necessary for deploying real-time Internet of Things deployments efficiently. As the importance of such scenarios is growing by the day, we propose to undertake two different kind of models, such as an algebraic models, with a process algebra called ACP and a coding model with a modeling language called Promela. Both approaches have been used to build models considering an edge infrastructure with a cloud backup, which has been further extended with the addition of extra fog nodes, and after having applied the proper verification techniques, they have all been duly verified. Specifically, a generic edge computing design has been specified in an algebraic manner with ACP, being followed by its corresponding algebraic verification, whereas it has also been specified by means of Promela code, which has been verified by means of the model checker Spin.
Autotuning Parallel Programs by Model Checking Garanina, Natalia Olegovna; Gorlatch, Sergei Petrovich
Modeling and Analysis of Information Systems,
12/2021, Letnik:
28, Številka:
4
Journal Article
Recenzirano
Odprti dostop
The paper presents a new approach to autotuning data-parallel programs. Autotuning is a search for optimal program settings which maximize its performance. The novelty of the approach lies in the use ...of the model checking method to find the optimal tuning parameters by the method of counterexamples. In our work, we abstract from specific programs and specific processors by defining their representative abstract patterns. Our method of counterexamples implements the following four steps. At the first step, an execution model of an abstract program on an abstract processor is described in the language of a model checking tool. At the second step, in the language of the model checking tool, we formulate the optimality property that depends on the constructed model. At the third step, we find the optimal values of the tuning parameters by using a counterexample constructed during the verification of the optimality property. In the fourth step, we extract the information about the tuning parameters from the counter-example for the optimal parameters. We apply this approach to autotuning parallel programs written in OpenCL, a popular modern language that extends the C language for programming both standard multi-core processors (CPUs) and massively parallel graphics processing units (GPUs). As a verification tool, we use the SPIN verifier and its model representation language Promela, whose formal semantics is good for modelling the execution of parallel programs on processors with different architectures.
All Internet of Things application layer protocols are built on top of the Medium Access Control layer (MAC layer). The MAC Layer’s primary goal is to limit or eliminate packet collisions. The ...technique of checking a protocol’s behavior that is represented by formal models is known as formal verification. Model checkers are used by protocol developers to automate the formal verification process because the human procedure of formal verification requires a great deal of mathematical concepts. This method uses model specification language to create formal models for the formal verification of protocols. The formal models’ temporal claims are used to specify the properties that need to be proved. If the property provided using temporal claims is not satisfied, the model checker uses these formal model and temporal claims and outputs a violating trace. There are only a few works that support the formal verification of MAC protocols. It’s because their behavior is difficult to abstract using model specification language. This paper suggests new abstraction methods in the form of algorithms for designing and modeling Time Division Multiple Access (TDMA) based scheduled MAC protocol using model specification language. Modeling links, superframes, multiple superframes, device schedules, and TDMA protocol abstraction are among the methods proposed. In order to support the applicability of the proposed methods, a TDMA-based formal model that meets the Wireless Highway Addressable Remote Transducer protocol specification requirements was created using PROMELA, a model specification language for SPIN model checker. In normal and constrained channel environments, the reachability of various marked states added into the model using temporal claims is verified. The verification result shows that the protocol performs as expected in a non-lossy channel environment. However, the protocol exhibits reliability issues due to message loss in a constrained channel environment. Finally, the model is checked for errors in design and message collisions. The results of the verification show that the model is free of design flaws and message collisions. The abstraction schemes proposed in this work help to quickly develop formal models for the verification of TDMA-based scheduled MAC protocols using model-checking tools.
Verification and Validation of railway controllers is the most critical and time-consuming phase in a system development life-cycle. It is regulated by international standards, which explicitly ...recommend the usage of state machines to model the specification of the system under test. Despite the great deal of works addressing the usage of state machines and their extensions, model-based verification and validation processes still lack concise and expressive-enough notations able to easily capture peculiar features of the specific domain of multi-process control systems, on which proper tool chains can be implemented in order to realize effective and automated environments.
This paper introduces a novel class of hierarchical state machines, called Dynamic STate Machines (DSTMs), and proposes an approach for modelling and validating railway control systems, based on the new specification language. Key features of DSTM are recursive execution, parallelism, parameter passing, abortion transition, and communication through global variables and channels, but its main peculiarity resides in the semantics of fork and join operators which allows for dynamic instantiation of machines (processes). The formal semantics of DSTM allows for the definition of verification and validation methodologies supported by automated tools. The paper also describes how DSTM specifications may be mapped to Promela models in order to achieve automated generation of test cases by model checking and Spin.
The work presented in this paper was carried out in the context of an European project and is strongly driven by the industrial necessity of tackling issues concerning the automation of functional system-level testing of modern railway signalling systems. Hence, the language and the proposed approach are illustrated and motivated by applying them to a specific functionality of the Radio Block Centre, the vital core of the ERTMS/ETCS Control System.
The advancement of the Internet of Things (IoT) has tremendously influenced many fields of human life. The Internet of Medical Things, Internet of Flying Things, Internet of Floating Things and ...Internet of Autonomous Things are recent evolution of IoT. The protocols used in all forms of IoT are critical during the execution demanding formal verification methods to ensure correctness. However, the most challenging part of formal verification is abstracting the system under test, making many systems unverified. Formal protocol verification is essential for detecting specification and design flaws that go undetected and corrected during the testing phase. This paper proposes novel methods for abstracting communication patterns for IoT protocols. Message broadcasts, periodic message advertisements, topology encoding, and topology change are examples of communication patterns. An attempt is made to model these patterns using
pi
-calculus and PROMELA. Finally, the trickle, a wireless sensor network dissemination protocol, has been modelled using
pi
-calculus and PROMELA. The Spin model checker verifies design flaws, such as deadlocks and non-progress cycles. The verification results ensure that there are no deadlocks or non-progress loops. The protocol is statically verified for message transmission semantics. The analysis revealed that the protocol could only guarantee message transmission for lossy connections if an alternative route covers all other nodes. The empirical results and theorem show that the abstraction mechanism can be directly utilised for automated and theoretical verification. Researchers can use the abstraction framework described in this paper to create validation models for static and automated verification of existing and new IoT protocols.
PDF
