Computation Tree Logic Model Checking of Multi-Agent Systems Based on Fuzzy Epistemic Interpreted Systems

Model checking is an automated formal verification method to verify whether epistemic multi-agent systems adhere to property specifications.Although there is an extensive literature on qualitative properties such as safety and liveness,there is still a lack of quantitative and uncertain property verifications for these systems.In uncertain environments,agents must make judicious decisions based on subjective epistemic.To verify epistemic and measurable properties in multi-agent systems,this paper extends fuzzy computation tree logic by introducing epistemic modalities and proposing a new Fuzzy Computation Tree Logic of Knowledge(FCTLK).We represent fuzzy multi-agent systems as distributed knowledge bases with fuzzy epistemic interpreted systems.In addition,we provide a transformation algorithm from fuzzy epistemic interpreted systems to fuzzy Kripke structures,as well as transformation rules from FCTLK formulas to Fuzzy Computation Tree Logic(FCTL)formulas.Accordingly,we transform the FCTLK model checking problem into the FCTL model checking.This enables the verification of FCTLK formulas by using the fuzzy model checking algorithm of FCTL without additional computational overheads.Finally,we present correctness proofs and complexity analyses of the proposed algorithms.Additionally,we further illustrate the practical application of our approach through an example of a train control system.

Identifying Counterexamples Without Variability in Software Product Line Model Checking

Product detection based on state abstraction technologies in the software product line(SPL)is more complex when compared to a single system.This variability constitutes a new complexity,and the counterexample may be valid for some products but spurious for others.In this paper,we found that spurious products are primarily due to the failure states,which correspond to the spurious counterexamples.The violated products correspond to the real counterexamples.Hence,identifying counterexamples is a critical problem in detecting violated products.In our approach,we obtain the violated products through the genuine counterexamples,which have no failure state,to avoid the tedious computation of identifying spurious products dealt with by the existing algorithm.This can be executed in parallel to improve the efficiency further.Experimental results showthat our approach performswell,varying with the growth of the system scale.By analyzing counterexamples in the abstract model,we observed that spurious products occur in the failure state.The approach helps in identifying whether a counterexample is spurious or genuine.The approach also helps to check whether a failure state exists in the counterexample.The performance evaluation shows that the proposed approach helps significantly in improving the efficiency of abstraction-based SPL model checking.

Review of Software Model-Checking Techniques for Dealing with Error Detection in Program Codes

Debugging software code has been a challenge for software developers since the early days of computer programming. A simple need, because the world is run by software. So perhaps the biggest engineering challenge is finding ways to make software more reliable. This review provides an overview of techniques developed over time in the field of software model checking to solve the problem of detecting errors in program code. In addition, the challenges posed by this technology are discussed and ways to mitigate them in future research and applications are proposed. A comprehensive examination of the various model verification methods used to detect program code errors is intended to lay the foundation for future research in this area.

基于Model Checking的系统脆弱性分析

基于规则的脆弱性分析技术依赖于对系统组件间关系的经验知识,系统复杂性、竞态条件、隐含假设等因素,使规则的生成异常困难。该文提出了采用NuSMV作为Model Checking执行机验证系统安全行为模型的脆弱性分析方法,并详细描述了对两个模型实例进行验证的过程。结果显示,这种方法具有识别已知和未知脆弱性的能力。

Model Checking-Based Testing of Web Applications

A formal model representing the navigation behavior of a Web application as the Kripke structure is proposed and an approach that applies model checking to test case generation is presented. The Object Relation Diagram as the object model is employed to describe the object structure of a Web application design and can be translated into the behavior model. A key problem of model checking-based test generation for a Web application is how to construct a set of trap properties that intend to cause the violations of model checking against the behavior model and output of counterexamples used to construct the test sequences. We give an algorithm that derives trap properties from the object model with respect to node and edge coverage criteria.

Model Checking Workflow Net Based on Petri Net

The soundness is a very important criterion for the correctness of the workflow. Specifying the soundness with Computation Tree Logic （CTL） allows us to verify the soundness with symbolic model checkers. Therefore the state explosion problem in verifying soundness can be overcome efficiently. When the property is not satisfied by the system, model checking can give a counter-example, which can guide us to correct the workflow. In addition, relaxed soundness is another important criterion for the workflow. We also prove that Computation Tree Logic ＊ （CTL ＊ ） can be used to character the relaxed soundness of the workflow.

Significance of three step prescription checking by pharmacists

In many hospitals,prescription checks are conducted by 2 or 3 individual pharmacists at each step of prescription checking,dispensing,and final checking to maintain the safety and efficacy of pharmaceutical therapies in Japan[1,2].In Gunma University Hospital,we also check all prescriptions by 3 pharmacists at each step of dispensing(3 step prescription check system)with the exception of night time.In this study,to assess the significance of our 3 step prescription check system for managing safety of pharmaceutical therapies,we investigated prescriptions that needed the confirmation of questionable points and prescription corrections.

Probabilistic Model Checking-Based Survivability Analysis in Vehicle-to-Vehicle Networks

Probabilistic model checking has been widely applied to quantitative analysis of stochastic systems, e.g., analyzing the performance, reliability and survivability of computer and communication systems. In this paper, we extend the application of probabilistic model checking to the vehicle to vehicle(V2V) networks. We first develop a continuous-time Markov chain(CTMC) model for the considered V2V network, after that, the PRISM language is adopted to describe the CTMC model, and continuous-time stochastic logic is used to describe the objective survivability properties. In the analysis, two typical failures are considered, namely the node failure and the link failure, respectively induced by external malicious attacks on a target V2V node, and interrupt in a communication link. Considering these failures, their impacts on the network survivability are demonstrated. It is shown that with increasing failure strength, the network survivability is reduced. On the other hand, the network survivability can be improved with increasing repair rate. The proposed probabilistic model checking-based approach can be effectively used in survivability analysis for the V2V networks, moreover, it is anticipated that the approach can be conveniently extended to other networks.

Analysis of Security of Quantum Key Distribution Based on Entangled Photon Pairs by Model Checking

Quantum key distribution is a technique to securely distribute a bit string between two parties by using the laws of quantum mechanics. The security of this technique depends on the basis of quantum mechanics rather than the difficulty of the mathematical calculation as in the classical encoding. Researches in this field have shown that the quantum key distribution will be fully functioning outside the laboratory in a few years. Due to the complexity and the high efficiency of the device, the verification is needed. In this article, we use PRISM to verify the security of the quantum key distribution protocol, which uses the entangled photon based on BB84 protocol.

Abstract Model Checking for Web Services

Web-services are highly distributed programs, and concurrent software is notoriously error-prone. Model checking is a powerful technique to find bugs in concurrent systems. However, the existing model checkers have no enough ability to support for the programming languages and communication mechanisms used for Web services. We propose to use Kripke structures as means of modeling Web service. This paper presents an automated way to extract formal models from programs implementing Web services using predicate abstraction for abstract model checking. The abstract models are checked by means of a model checker that implements automatic abstraction refinement. These results enable the verification of the applications that implement Web services.

Subsumption Checking between Concept Queries in Different Ontologies Based on Mutual Instances

This paper proposes a checking method based on mutual instances and discusses three key problems in the method： how to deal with mistakes in the mutual instances and how to deal with too many or too few mutual instances. It provides the checking based on the weighted mutual instances considering fault tolerance, gives a way to partition the large-scale mutual instances, and proposes a process greatly reducing the manual annotation work to get more mutual instances. Intension annotation that improves the checking method is also discussed. The method is practical and effective to check subsumption relations between concept queries in different ontologies based on mutual instances.

Generating test case specifications of web service composition using model checking

Model checking techniques have been widely used in verifying web service compositions to ensure the trustworthi- ness. However, little research has focused on testing web services. Based on the research of model checking techniques~ we propose a model checking based approach for testing web service composition which is described by using the web services choreography description language （WS-CDL）. According to worldwide web consortium （W3C） candidate recommendation, the WS-CDL specification provides a language for characterizing interactions between distinct web services using XML. Since the behaviors of web service composition are asynchronous, distributed, low-coupled and platform independent, we employ the guarded automata （GA） model for specifying the composition described in WS-CDL and using the simple promela interpreter （SPIN） model checker for detecting the collaborations of web services. Test cases can be transformed from counterexamples generated by SPIN using adequacy criteria. In this paper we apply the transition coverage criterion for generating counterex- amples. To illustrate our approach, we set ＂E-commerce service system＂ as an example for demonstrating how test cases can be generated using SPIN for compositions specified in WS-CDL.

Model checking web services choreography in process analysis toolkit

Web service （WS） is an emerging software technology, especially acting an important role in cloud computing. The WS choreography description language （WS-CDL） is the standard for modeling the observable behavior of WS composition across multiple participants from a global point of view. However, it lacks of a formal semantics and could easily lead to misunderstanding and different implementations. In this paper, the WS-CDL based specifications are formally extracted in a communicating sequential process supporting a formal approach to checking WS models. In addition, formalisms and model checking are explicitly illustrated through a simple but non-trivial example with the help of model checker process analysis toolkit （PAT）.

Image Betrayal Checking Based on the Digital Fingerprint of Images on the Internet

In the Internet environment, documents are easily leaked, and divulged files spread rapidly. Therefore, it is important for privacy institutions to actively check the documents on the Internet to find out whether some private files have been leaked. In this paper, we put forward a scheme for active image betrayal checking on the Intemet based on the digital fingerprint, which embeds fingerprints into privacy documents, extracts codes from the Intemet images, and then fmds out the divulged files by matching two groups of codes. Due to so many documents on the Internet, the number of times of code comparison is huge, which leads to a large running time. To overcome the deficiency in practical application, we optimized the process by accurate matching methods and approximate matching method. Then a method was proposed to group objects by locality sensitive hashing （LSH） process before code comparison, in order to eliminate the vast majority of unrelated pairs. Experiments prove that this method could operate with less running time and less memory.

A Spell Checking Web Service API for Smart City Communication Platforms

The Internet of Things becomes Internet of Everything when in the process of communication machine-to-machine also intelligent forms of communication between human and machine are involved. Cities can be viewed as a microcosm of this interconnected system where ICT and emerging technologies can be enabling factors to transform cities in Smart Cities. Cities can take great advantage by using information intelligence to achieve important public-policy goals and, in particular, by enabling network communication channels between citizens and public administrators in order to provide information and online services in real time through platform systems rather than by means of humans, using Artificial Intelligence and Natural Language Processing techniques. This work was the first step of a wider project aimed at providing a Spell Checking Web Service API for Smart City communication platforms able to automatically select, among the large availability of open source spell checking tools, the most suitable tool based on the semantic structure of the specific textual data. The system should manage an enhanced Italian Vocabulary Database, specifically implemented to support all the tools of the system. The goal of the present work was to test, through an experimental research, the feasibility of the entire project by implementing a Spell Checking Prototype System designed to manage two selected spell checking tools. Results showed that the Spell Checking Prototype System significantly improves performances by allowing the user to select the most suitable tool for the specific semantic structure of the text. The system also enables to manage the list of exceptions, which continuously enhance the Italian Vocabulary Database. The experimentation proved scientific evidence of the validity of the project aimed at implementing a Spell Checking Web Service API in order to improve the quality of natural language data to be stored or processed in Smart City NCeSDP systems, through the use of existing spell checking tools.

PLC Modeling and Checking Based on Formal Method

High reliability is the key to performance of electrical control equipment. PLC combines computer technology, automatic control technology and communication technology and becomes widely used for automation of industrial processes. Some requirements of complex PLC systems cannot be satisfied by the traditional verification methods. In this paper, an efficient method for the PLC systems modeling and verification is proposed. To ensure the high-speed property of PLC, we proposed a technique of “Time interval model” and “notice-waiting”. It could reduce the state space and make it possible to verify some complex PLC systems. Also, the conversion from the built PLC model to the Promela language is obtained and a tool PLC-Checker for modeling and checking PLC systems are designed. Using PLC-Checker to check a classical PLC example, a counter-example is found. Although the probability of this logic error occurs very small, it could result in system crash fatally.

Timed-Automata Based Model-Checking of a Multi-Agent System: A Case Study

A multi-agent based transport system is modeled by timed automata model extended with clock variables. The correctness properties of safety and liveness of this model are verified by timed automata based UPPAAL. Agents have a degree of control on their own actions, have their own threads of control, and under some circumstances they are also able to take decisions. Therefore they are autonomous. The multi-agent system is modeled as a network of timed automata based agents supported by clock variables. The representation of agent requirements based on mathematics is helpful in precise and unambiguous specifications, thereby ensuring correctness. This formal representation of requirements provides a way for logical reasoning about the artifacts produced. We can be systematic and precise in assessing correctness by rigorously specifying the functional requirements.

The Design of Circuit for Checking Short in HT-7U Superconducting Tokamak Device

The tokamak HT-7U project has been funded as a Chinese national project since 1998. The main object of the project is to build a nuclear fusion experimental device with divertor configuration, which is designed by the Institute of Plasma Physics, the Chinese Academy of Sciences (ASIPP). It is a full superconducting device, consisting of superconducting toroidal field (TF) coils and superconducting poloidal field (PF) coil. During the operation of the device, the operational parameter of device should be checked by technical diagnosis. This paper describes the design of circuit for checldng short between every two parts of the HT7U device. The main contents of design include circuit of data acquisition and data processing of computer.

NEW REGULATIONS OF CHECKING AND WRITING-OFF FOREIGN EXCHANGE PAYMENT FOR TRADE IMPORT

As from March 1,the State Administration of Exchange Con-trol will implement a new "Provisional Regulations of Checking,Writing-off and Supervising Foreign Exchange Payment for TradeImport".This is an important measure of reforming China’s for-eign exchange system, and is an afterwards supervising measure ofguaranteeing orderly proceeding of toreign exchange payment fortrade import after the exchange of regular items.One of the purpose of carrying out the new regulations is toform an afterwards supervising mechanism for foreign exchangeimport payment of regular items which guarantees the authenticityof foreign exchange import payment and orderly proceeding theexchange of Renminbi regular items;secondly,through examiningand verifying documents of foreign exchange import payment,veri-

Checking of Radially Sawn Scots Pine and Norway Spruce Wood

In exterior use, wood is subjected to weathering that causes checking and other deterioration in the appearance and technical properties. We studied quantitatively the surface checking of radially and tangentially sawn specimens of Scots pine (Pinus sylvestris L.) and Norway spruce (Picea abies Karst.) wood in a cyclic climate chamber test. The results strongly suggested that the sawing direction determines the checking performance of both Scots pine and Norway spruce wood. The radial surface of Scots pine specimens had 62% less checks than the tangential one, and the cumulative area of checks was 74% smaller. For Norway spruce, the respective figures were: 83% less in the check number and 91% less in the check area. Different from pine, in spruce specimens the checks of radial surface were significantly smaller. Thus, spruce timber gained clearly more about radial sawing pattern. The effect of annual ring width was similar for pine and spruce: the reduction in annual growth worsened the checking. The increase in density worsened the checking of spruce but did not change the performance of pine. In pine wood, the increase of heartwood proportion reduced the fluctuation of moisture content and the formation of checks.