检索结果-南通市图书馆

formal verification of Temporal Properties for Reduced Overhead in Grid Scientific Workflows

在线全文

学校读者我要写书评

暂无评论

Journal of Computer Science & Technology 2011年第6期26卷 1017-1030页

作者：曹军威张帆许可刘连臣吴澄 CCF ACM IEEE Research Institute of Information Technology Tsinghua University Tsinghua National Laboratory for Information Science and Technology National CIMS Engineering and Research Center Tsinghua University Morgan Stanley

With quick development of grid techniques and growing complexity of grid applications, it is becoming critical for reasoning temporal properties of grid workflows to probe potential pitfalls and errors, in order to ensure reliability and trustworthiness at the initial design phase. A state Pi calculus is proposed and implemented in this work, which not only enables fexible abstraction and management of historical grid verification of grid workflows. Furthermore, a relaxed region system events, but also facilitates modeling and temporal analysis （RRA） approach is proposed to decompose large scale grid workflows into sequentially composed regions with relaxation of parallel workflow branches, and corresponding verification strategies are also decomposed following modular verification principles. Performance evaluation results show that the RRA approach can dramatically reduce CPU time and memory usage of formal verification.

关键词： grid computing workflow management formal verification state Pi calculus

formal verification of Data Modifications in Cloud Block Storage Based on Separation Logic

在线全文

学校读者我要写书评

暂无评论

Chinese Journal of Electronics 2024年第1期33卷 112-127页

作者： Bowen ZHANG Zhao JIN Hanpin WANG Yongzhi CAO Key Laboratory of High Confidence Software Technologies (MOE) School of Computer Science Peking University School of Computer and Artificial Intelligence Zhengzhou University School of Computer Science and Cyber Engineering Guangzhou University

Cloud storage is now widely used, but its reliability has always been a major concern. Cloud block storage(CBS) is a famous type of cloud storage. It has the closest architecture to the underlying storage and can provide interfaces for other types. Data modifications in CBS have potential risks such as null reference or data *** verification of these operations can improve the reliability of CBS to some extent. Although separation logic is a mainstream approach to verifying program correctness, the complex architecture of CBS creates some challenges for verifications. This paper develops a proof system based on separation logic for verifying the CBS data modifications. The proof system can represent the CBS architecture, describe the properties of the CBS system state, and specify the behavior of CBS data modifications. Using the interactive verification approach from Coq, the proof system is implemented as a verification tool. With this tool, the paper builds machine-checked proofs for the functional correctness of CBS data modifications. This work can thus analyze the reliability of cloud storage from a formal perspective.

关键词： Cloud computing Behavioral sciences Reliability formal verification

formal verification Platform as a Service:WebAssembly Vulnerability Detection Application

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Computer Systems Science & Engineering 2023年第5期45卷 2155-2170页

作者： LiangJun Deng Hang Lei Zheng Yang WeiZhong Qian XiaoYu Li Hao Wu Sihao Deng RuChao Sha WeiDong Deng School of Information and Software Engineering University of Electronic Science and Technology of ChinaChengdu610054China School of Physics University of Electronic Science and Technology of ChinaChengdu611731China ICB-PMDM-LERMPS UMR 6303 CNRSUTBMUniversitéde Bourgogne Franche-ComtéBelfort90010France Chengdu Railway Science and Technology Innovation Co.LTD Chengdu640041China

In order to realize a general-purpose automatic formal verification platform based on WebAssembly technology as a web service(FVPS),which aims to provide an automated report of vulnerability detections,this work builds a Hyperledger Fabric blockchain runtime *** proposes an optimized methodology of the functional equivalent translation from source program languages to formal *** methodology utilizes an external application programming interface(API)table to replace the source codes in compilation,thereby pruning the part of housekeeping codes to ease code *** inflation is a significant metric in formal language ***,minor code inflation enhances verification scale and performance *** determines the efficiency of formal verification,involving launching,running,and memory *** instance,path explosion increases exponentially,resulting in *** experimental results conclude that program languages like golang severely impact code *** reduces the wasm code size by over 90%,achieving two orders of optimization magnitude,from 2000 kilobyte(KB)to 90 *** means we can cope with golang applications up to 20 times larger than the original in *** work eliminates the gap between Hyperledger Fabric smart contracts and *** approach is pragmatic,adaptable,extendable,and ***,FVPS is successfully applied in a Railway-Port-Aviation blockchain transportation system.

关键词： WebAssembly formal verification blockchain smart contract

formal verification under Unknown Constraints

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Wuhan University Journal of Natural Sciences 2005年第1期10卷 43-46页

作者： LI Guang-hui 1,2,3 , LI Xiao-wei 2,31. School of Information Engineering, Zhejiang Forestry College, Hangzhou 311300, Zhejiang, China 2. Institute of Computing Technology, Chinese Academy of Sciences, Beijing 100080, China 3. Graduate School of the Chinese Academy of Sciences, Beijing 100039, China School of Information Engineering Zhejiang Forestry College Hangzhou Zhejiang China Institute of Computing Technology Chinese Academy of Sciences Beijing China Graduate School of the Chinese Academy of Sciences Beijing China

We present a formal method of verifying designs with unknown constraints (e.g., black boxes) using Boolean satisfiability (SAT). This method is based on a new encoding scheme of unknown constraints, and solves the corresponding conjunctive normal form (CNF) ***,this method can avoid the potential memory explosion, which the binary decision diagram (BDD) based techniques maybe suffer from, thus it has the capacity of verifying large designs. Experimental results demonstrate the efficiency and feasibility of the proposed method.

关键词： formal verification unknown constraints black box Boolean satisfiability Boolean comparison

formal verification of TASM Models by Translating into UPPAAL

在线全文

学校读者我要写书评

暂无评论

Journal of Donghua University(English Edition) 2012年第1期29卷 51-54页

作者：胡凯张腾杨志斌顾斌蒋树姜泮昌 School of Computer Science and Engineering Beihang University Beijing Institute of Control Engineering

Timed abstract state machine(TASM) is a formal specification language used to specify and simulate the behavior of real-time systems. formal verification of TASM model can be fulfilled through model checking activities by translating into UPPAAL. Firstly, the translational semantics from TASM to UPPAAL is presented through atlas transformation language(ATL). Secondly, the implementation of the proposed model transformation tool TASM2UPPAAL is provided. Finally, a case study is given to illustrate the automatic transformation from TASM model to UPPAAL model.

关键词： timed abstract state machine(TASM) formal verification model transformation atlas transformation language(ATL) UPPAAL

Design and formal verification of a CEM protoco with transparent TTP

在线全文

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2013年第2期7卷 279-297页

作者： Zhiyuan LIU Jun PANG Chenyi ZHANG School of Management Science and Engineering Shandong Normal UniversityChina Jinan 250000 Faculty of Science Technology and Communication University of LuxembourgLuxembourg Luxembourg 1359 School of Information Technology and Electrical Engineering University of Queensland Australia Brisbane QLD4072

In certified email （CEM） protocols, trusted third party （TTP） transparency is an important security require- ment which helps to avoid bad publicity as well as protecting individual users＇ privacy. Cederquist et al. proposed an opti- mistic certified email protocol, which employs key chains to reduce the storage requirement of the TTE We extend their protocol to satisfy the property of TTP transparency, using existing verifiably encrypted signature schemes. An imple- mentation with the scheme based on bilinear pairing makes our extension one of the most efficient CEM protocols satis- fying strong fairness, timeliness, and TTP transparency. We formally verify the security requirements of the extended pro- tocol. The properties of fairness, timeliness and effectiveness are checked in the model checker Mocha, and TTP trans- parency is formalised and analysed using the toolsets/~CRL and CADE

关键词： fair exchange CEM protocols fairness TTPtransparency formal verification

Research on Microkernel Integrity Semantics Model and formal verification

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Chinese Journal of Electronics 2014年第1期23卷 43-48页

作者： QIAN Zhenjiang LIU Wei HUANG Hao State Key Laboratory for Novel Software Technology Nanjing University Department of Computer Science and Technology Nanjing University

Microkernel integrity is an important aspect of security for the whole microkernel system. Many of the research works on microkernel integrity focus on analysis and safeguards against the existing kernel attacks, and security enhancements for the vulnerabilities of system design and implementation aspects. The formal methods for operating system design and verification ensure the system’s high level of security. The existing formalization work and research for operating system mainly focus on the code-level verification of program correctness. In this paper, we propose a formal abstraction model of microkernel in order to accurately describe the semantics of every kernel behavior, and achieve the description of the whole kernel. Based on the model we illustrate the microkernel integrity criterions and elaborate on the integrity mechanism. Meanwhile, we formally verify the completeness and consistency between the mechanism and the definition of the microkernel integrity. We use the self-implemented operating system VTOS(Verified trusted operating system) as an example to illustrate the design method for the microkernel integrity.

关键词： Microkernel integrity Integrity mechanism Integrity semantics model formal verification

Cloud Manufacturing Service Composition Modeling and formal verification Based on Calculus for Orchestration of Web Service

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Cloud Manufacturing Service Composition Modeling and Formal ...

formal verification of the Merchant Registration Phase of the SET Protocol

第25届中国控制与决策会议

作者： LI Yongxiang YAO Xifan ZHANG Jie LI Bin School of Mechanical & Automotive Engineering South China University of Technology State Key Laboratory of Automotive Simulation and Control Jilin University

ISBN: (纸本)9781467355339

To solve the problem of modeling and formally verifying the composition of cloud manufacturing services, a new modeling and formal verification approach based on Calculus for Orchestration of Web Service （COWS） combined with Unified Modeling Language （UML） was proposed. First UML activity diagram for Cloud Manufacturing service composition was built with MagicDraw software, and saved as an XML file. The XML file was translated into a COWS file via UML4SOA, and formally verified with COWS Model Checking program （CMC）. Furthermore, a composite service about part processing was given. Activity diagram of the service composition was built, including milling service, drilling service, exception handling, event handling and compensation mechanism. Finally, the composition verification result showed that the proposed approach was feasible.

关键词： Calculus for Orchestration of Web service Cloud manufacturing Service composition Modeling formal verification

来源： cnki会议评论

在线全文

cnki会议

学校读者我要写书评

暂无评论

International Journal of Automation and computing 2005年第2期2卷 155-162页

作者： Xiao-Qi Ma Xiao-Chun Cheng Department of Computer Science The University of Reading Reading UK

This paper describes the formal verification of the Merchant Registration phase of the Secure Electronic Transactions (SET) protocol, a realistic electronic transaction security protocol which is used to protect the secrecy of online purchases. A number of concepts, notations, functions, predicates, assumptions and rules are introduced. We describe the knowledge of all legal participants, and a malicious spy, to assess the security of the sub-protocol. Avoiding search in a large state space, the method converges very quickly. We implemented our method in the Isabelle/Isar automated reasoning environment, therefore the whole verification process can be executed mechanically and efficiently. Keywords formal verification - electronic transaction protocol - knowledge-based system This work was supported by EC, EPSRC, the National Natural Science Foundation of China (No.60496320, 60496321), and Hong Kong K C Wang Education Foundation.Xiao-Qi Ma graduated from Nanjing University of Science and Technology, China, in 1997. He received his Master’s degree from the Institute of Software, Chinese Academy of Sciences in 2003. He is currently a PhD student at the University of Reading. His research interests include computer network security, knowledge-based systems, and operating systems.Xiao-Chun Cheng obtained his PhD in 1996. He has worked as a lecturer at the University of Reading since 2000. He is a guest professor at North East Normal University and Beijing Normal University. His research interests include theoretical and applied aspects in decision support systems, knowledge-based systems and intelligent systems.

关键词： formal verification electronic transaction protocol knowledge-based system