Formal verification and implementation of safety computer communication management mechanism by Liang LIANG, Yuan CAO, Lian-chuan MA, Yu-zhuo ZHANG, Heng-kui LI

Subjects: Get full text

Firmware vulnerability analysis based on formal verification of software and hardware by Peng-hui ZHANG, Xi TIAN, Kang-wei LOU

Subjects: Get full text

Design, implementation and formal verification of BGP proxy for mimic router by Jin ZHANG, Qiang GE, Weihai XU, Yiming JIANG, Hailong MA, Hongtao YU

Subjects: Get full text

Formal Verification of Nonfunctional Requirements of Overall Instrumentation and Control Architectures by Polina Ovsiannikova, Antti Pakonen, Dmitry Muromsky, Maksim Kobzev, Viktor Dubinin, Valeriy Vyatkin

“…In this article, we focus on the latter and use formal verification methods to reason about the correctness of an I&C architecture represented with an ontology, using the example of a nuclear power plant design. …”
Get full text

Formal Verification of ERC-Based Smart Contracts: A Systematic Literature Review by Rim Ben Fekih, Mariam Lahami, Salma Bradai, Mohamed Jmaiel

Subjects: Get full text

Formal Verification Method for Configuration of Integrated Modular Avionics System Using MARTE by Lisong Wang, Miaofang Chen, Jun Hu

“…Then we present a formal verification framework for ARINC653 system configuration based on theorem proof techniques, including construction of corresponding REAL theorems according to the semantics of those key components of configuration information and formal verification of theorems for the properties of IMA, such as time constraints, spatial isolation, and health monitoring. …”
Get full text

Formal Verification of Multi-Thread Minimax Behavior Using mCRL2 in the Connect 4 by Diego Escobar, Jesus Insuasti

“…This study focuses on the formal verification of a parallel version of the minimax algorithm using the mCRL2 modeling language, applied to the game of Connect 4. …”
Get full text

A Framework for the Generation of Monitor and Plant Model From Event Logs Using Process Mining for Formal Verification of Event-Driven Systems by Midhun Xavier, Victor Dubinin, Sandeep Patil, Valeriy Vyatkin

Subjects: Get full text

A Formal Approach to Road Safety Assessment Using Traffic Conflict Techniques by Oumaima Barhoumi, Mohamed H. Zaki, Sofiene Tahar

Subjects: Get full text

Functionally-Equivalent Formalization and Automated Model Checking of Function Block Diagrams by Tomas Ausberger, Karel Kubicek, Pavla Medvedcova

Subjects: Get full text

An integrated modeling, verification, and code generation for uncrewed aerial systems: less cost and more efficiency by Jianyu Zhang, Long Zhang, Yixuan Wu, Linru Ma, Feng Yang

Subjects: Get full text

End-to-End Framework for Identifying Vulnerabilities of Operational Technology Protocols and Their Implementations in Industrial IoT by Matthew Boeding, Michael Hempel, Hamid Sharif

Subjects: Get full text

Verification of serialising instructions for security against transient execution attacks by Kushal K. Ponugoti, Sudarshan K. Srinivasan, Nimish Mathure

Subjects: Get full text

Research on formal description and verification of automated trust negotiation by GUAN Shang-yuan 1, WU Wei-guo 1, DONG Xiao-she 1, QIAN De-pei1

“…First,a unified ATN formal framework was presented,into which typical negotiation strategies could be reduced.Second,the formal verification of ATN was defined based on the formal framework.The objectives and procedures of the formal verification of ATN were described.Third,several typical negotiation strategies were discussed,and the computational complexity of the corresponding verification problems was shown,several conclusions had been obtained.Last,the formal verification of ATN was implemented by using logic programming and model checking methods.The experimental results show that the number of rules is a crucial factor in determining the runtime.Both logic programming and model checking are efficient when the number of transition rules is small,and logic programming does not scale as well as model checking.…”
Get full text

Survey on model checking based hardware Trojan detection technology by Qizhi ZHANG, Yiqiang ZHAO, Ya GAO, Haocheng MA

“…Hardware Trojan is malicious tampering to the original circuit, which has become the most important security threat of integrated circuit.In order to ensure the safety and reliability of ICs, many hardware Trojan detection methods are proposed.As one of the formal verification methods, model checking can effectively detect the hardware Trojan in the design phase.Firstly, the working principle and process of model checking were described.Secondly, the research progress of hardware Trojan detection technology based on model checking was introduced.Finally, the bottlenecks faced by the current technology were pointed out and the potential research direction was discussed.…”
Get full text

Formalization of Linear Space Theory in the Higher-Order Logic Proving System by Jie Zhang, Danwen Mao, Yong Guan

“…Theorem proving is an important approach in formal verification. Higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and stronger semantics. …”
Get full text

Probabilistic Model Checking: One Step Forward in Wireless Sensor Networks Simulation by José A. Mateo, Hermenegilda Macià, M. Carmen Ruiz, Javier Calleja, Fernando Royo

“…Thus, all the benefits of formal verification and simulation are gathered. These correctness properties as well as practical and relevant scenarios for the real world have agreed with the algorithm designers.…”
Get full text

Research on verification of behavior requirement patterns based on action sequences by DU Jun-wei1, XU Zhong-wei2, JIANG Feng1

“…Function behavior requirements（FBR） and safety behavior requirements（SBR） were described by action se-quences.Compared with the traditional logic or graphic form,action sequences can express the temporal relationship among interactive behaviors more exactly.Moreover,FBR pattern and SBR pattern are constructed by action sequences,and the operation semantics of these patterns are also given.To implement the requirement verification based on behavior patterns,the necessary and sufficient conditions as well as the checking algorithm for the satisfiability of FBR pattern and SBR pattern are presented and proven by redefining the property expression and combination operation of LTS’s safety and liveness.The framework has been widely applied in the formal verification ＆ validation of component-based CTCS2/3 systems,and has shown great theoretical and practical significance to combinational verification of Compo-nent-based safety-critical systems.…”
Get full text

Secure and efficient group handover authentication protocol based on trajectory prediction in 5G-V2X by Yinghui ZHANG, Jiale QIAN, Jin CAO, Dong ZHENG

“…Aiming at the efficiency issue of handover authentication for a large number of vehicles in the 5G-V2X scenario, a secure and efficient group handover authentication protocol based on trajectory prediction was proposed.Firstly, the effect of completing key agreement protocol in advance was achieved by predicting vehicle trajectories.Secondly, vehicles with mobility relevance were treated as the same group through user grouping algorithms, and then all vehicles within the group were batch verified using certificateless aggregation signature technology.In addition, to address the vulnerability of aggregated signature technology to DoS attacks, a binary search method was used to quickly locate malicious users and improve the efficiency of group handover authentication protocol.Finally, the security analysis of the protocol was conducted using the formal verification tool Scyther, and compared with the existing optimal protocol, the computational efficiency is improved by 30%.…”
Get full text

Research on Access Authentication and Re-Authentication Mechanism of User Devices in Terrestrial Default Scenario in Satellite Internet by Qiuyu BU, Jin CAO, Lifu CHENG, Ruhui MA, Hui LI

“…For the current user device access authentication mechanism requires ground participation to bring about large communication delays and poor scalability, a user device access authentication and re-authentication protocol in the ground default scenario in the space-ground integrated network was proposed, and further for the user device authentication process may occur in the power outage reconnection and AV asynchronization and other problems, a user device fast authentication mechanism and AV fast security synchronization mechanism under power failure reconnection scenario were proposed to ensured that users could safely accessed the satellite network and obtain related services.In the proposed scheme, the AV vector generated in the initial access authentication was used to assisted the re-authentication process to completed the authentication between entities without the involvement of the network control center, which guaranteed the communication system resilience.The formal verification tool Scyther showed that the proposed protocol was resistant to common protocol attacks, guaranteed the confidentiality and integrity of the communication process, and had a small signaling, computational, and bandwidth overhead, made it suitable for the satellite internet.…”
Get full text