Counterexample-Preserving Reduction for Symbolic Model Checking by Wanwei Liu, Rui Wang, Xianjin Fu, Ji Wang, Wei Dong, Xiaoguang Mao

“…The cost of LTL model checking is highly sensitive to the length of the formula under verification. …”
Get full text

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

“…This article presents a new method based on functionally-equivalent formalisation and model checking. This method can be used for automatic verification of I&C algorithms by model checking while preserving obtained proofs from a formalised model in the original algorithm. …”
Get full text

Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives by Rui Wang, Wanwei Liu, Tun Li, Xiaoguang Mao, Ji Wang

“…As a complementary technique of the BDD-based approach, bounded model checking (BMC) has been successfully applied to LTL symbolic model checking. …”
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

“…A novel collision resolution algorithm for wireless sensor networks is formally analysed via probabilistic model checking. The algorithm called 2CS-WSN is specifically designed to be used during the contention phase of IEEE 802.15.4. …”
Get full text

Concurrent software fine‐coarse‐grained automatic modelling by Coloured Petri Nets for model checking by Wenjie Zhong, Jian‐tao Zhou, Tao Sun

“…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. …”
Get full text

Verification and Optimal Control of Context-Sensitive Probabilistic Boolean Networks Using Model Checking and Polynomial Optimization by Koichi Kobayashi, Kunihiko Hiraishi

Get full text

A Latent Implementation Error Detection Method for Software Validation by Jiantao Zhou, Jing Liu, Jinzhao Wu, Guodong Zhong

“…Model checking and conformance testing play an important role in software system design and implementation. …”
Get full text

Modeling and Analyzing CSMA/CA Protocol for Energy-Harvesting Wireless Sensor Networks by Zhi Chen, Ya Peng, Wenjing Yue

“…This paper models the MAC protocol of CSMA/CA using timed automata on the message communication and the energy harvesting and analyzes the protocol through model checking of the major CTL properties. The modeling and analysis of CSMA/CA protocol with the comparative experiments give some performance results and also reveal that timing error may cause deadlock, and the accessibility is satisfied if no deadlock exists.…”
Get full text

Digital rule-based compliance processes. The urban regeneration of ex-Corradini, Naples (IT) by Marina Rigillo, Sergio Russo Ermolli, Giuliano Galluccio

“…The application of BIM-based procedures in the early design process stage becomes an opportunity to develop a multi-scenario approach, which employs Code and Model Checking systems as ‘heuristic’ tools to support decisions and enhancing risk management in complex projects.…”
Get full text

Automatic Analysis of Complex Interactions in Microservice Systems by Fei Dai, Hao Chen, Zhenping Qiang, Zhihong Liang, Bi Huang, Leiguang Wang

“…In this paper, we propose an approach for interaction analysis using model checking techniques, which is supported by the Process Analysis Toolkit (PAT) tool. …”
Get full text

Dilemma of Responsibility-Sensitive Safety in Longitudinal Mixed Autonomous Vehicles Flow: A Human-Driver-Error-Tolerant Driving Strategy by Hongsheng Qi

“…Responsibility sensitive safety (RSS) is proposed to serve as a model checking tool for AV safety. However, RSS alone cannot guarantee safety when they are mixed with human-driven vehicles (HDVs). …”
Get full text

Research on Operation Characteristics and Safety Risk Forecast of Bus Driven by Multisource Forewarning Data by Shejun Deng, Hongru Yu, Caoye Lu

“…To prevent and control public transport safety accidents in advance and guide the safety management and decision-making optimization of public transport vehicles, based on the forewarning and other multisource data of public transport vehicles in Zhenjiang, holographic portraits of public transport safety operation characteristics are constructed from the perspectives of time, space, and driver factors, and a prediction model of fatigue driving and driving risk of bus drivers based on BP neural network is constructed. Finally, model checking and virtual simulation experiments are carried out. …”
Get full text