期刊文献+
共找到40篇文章
< 1 2 >
每页显示 20 50 100
Integrating object-oriented methods and formal methods for requirement engineering 被引量:1
1
作者 陈怡海 缪淮扣 《Journal of Harbin Institute of Technology(New Series)》 EI CAS 2004年第3期295-299,共5页
High quality software requirement specification is crucial for a software development. Although much efforts and research works have been done to address the problem, the errors in user requirement are still prevent u... High quality software requirement specification is crucial for a software development. Although much efforts and research works have been done to address the problem, the errors in user requirement are still prevent us from developing high quality software. To address the problem, this paper proposes integrating graphical specification technique UML with formal specification technique to construct user requirement specification. We also present a prototype tool to perform the automatic translation from UML specification into Object-Z specification. 展开更多
关键词 formal methods UML OBJECT-Z methods integration
下载PDF
On the use of formal methods to model and verify neuronal archetypes
2
作者 Elisabetta DE MARIA Abdorrahim BAHRAMI +4 位作者 Thibaud L'YVONNET Amy FELTY Daniel GAFFÉ Annie RESSOUCHE Franck GRAMMONT 《Frontiers of Computer Science》 SCIE EI CSCD 2022年第3期101-122,共22页
Having a formal model of neural networks can greatly help in understanding and verifying their properties,behavior,and response to external factors such as disease and medicine.In this paper,we adopt a formal model to... Having a formal model of neural networks can greatly help in understanding and verifying their properties,behavior,and response to external factors such as disease and medicine.In this paper,we adopt a formal model to represent neurons,some neuronal graphs,and their composition.Some specific neuronal graphs are known for having biologically relevant structures and behaviors and we call them archetypes.These archetypes are supposed to be the basis of typical instances of neuronal information processing.In this paper we study six fundamental archetypes(simple series,series with multiple outputs,parallel composition,negative loop,inhibition of a behavior,and contralateral inhibition),and we consider two ways to couple two archetypes:(i)connecting the output(s)of the first archetype to the input(s)of the second archetype and(ii)nesting the first archetype within the second one.We report and compare two key approaches to the formal modeling and verification of the proposed neuronal archetypes and some selected couplings.The first approach exploits the synchronous programming language Lustre to encode archetypes and their couplings,and to express properties concerning their dynamic behavior.These properties are verified thanks to the use of model checkers.The second approach relies on a theorem prover,the Coq Proof Assistant,to prove dynamic properties of neurons and archetypes. 展开更多
关键词 neuronal networks leaky integrate and fire modeling synchronous languages model checking theorem proving LUSTRE COQ formal methods
原文传递
Formal methods, statistical debugging and exploratory analysis in support of system development: Towards a verification and validation calculator tool
3
作者 Saikou Y.Diallo Ross Gore +1 位作者 Christopher J.Lynch Jose J.Padilla 《International Journal of Modeling, Simulation, and Scientific Computing》 EI 2016年第1期120-141,共22页
In this paper,we propose an approach to formally verify and rigorously validate a simulation system against the specification of the real system.We implement the approach in a verification and validation calculator to... In this paper,we propose an approach to formally verify and rigorously validate a simulation system against the specification of the real system.We implement the approach in a verification and validation calculator tool that takes as input a set of statements that capture the requirements,internal conditions of the system and expected outputs of the real system and produces as output whether the simulation satisfies the requirements,faithfully represents the internal conditions of the system and produces the expected outputs.We provide a use case to show how subject matter experts can apply the tool. 展开更多
关键词 Verification and validation formal methods modeling and simulation
原文传递
MF2-DMTD: A Formalism and Game-Based Reasoning Framework for Optimized Drone-Type Moving Target Defense
4
作者 Sang Seo Jaeyeon Lee +2 位作者 Byeongjin Kim Woojin Lee Dohoon Kim 《Computers, Materials & Continua》 SCIE EI 2023年第11期2595-2628,共34页
Moving-target-defense(MTD)fundamentally avoids an illegal initial compromise by asymmetrically increasing the uncertainty as the attack surface of the observable defender changes depending on spatial-temporal mutation... Moving-target-defense(MTD)fundamentally avoids an illegal initial compromise by asymmetrically increasing the uncertainty as the attack surface of the observable defender changes depending on spatial-temporal mutations.However,the existing naive MTD studies were conducted focusing only on wired network mutations.And these cases have also been no formal research on wireless aircraft domains with attributes that are extremely unfavorable to embedded system operations,such as hostility,mobility,and dependency.Therefore,to solve these conceptual limitations,this study proposes normalized drone-type MTD that maximizes defender superiority by mutating the unique fingerprints of wireless drones and that optimizes the period-based mutation principle to adaptively secure the sustainability of drone operations.In addition,this study also specifies MF2-DMTD(model-checkingbased formal framework for drone-type MTD),a formal framework that adopts model-checking and zero-sum game,for attack-defense simulation and performance evaluation of drone-type MTD.Subsequently,by applying the proposed models,the optimization of deceptive defense performance of drone-type MTD for each mutation period also additionally achieves through mixed-integer quadratic constrained programming(MIQCP)and multiobjective optimization-based Pareto frontier.As a result,the optimal mutation cycles in drone-type MTD were derived as(65,120,85)for each control-mobility,telecommunication,and payload component configured inside the drone.And the optimal MTD cycles for each swarming cluster,ground control station(GCS),and zone service provider(ZSP)deployed outside the drone were also additionally calculated as(70,60,85),respectively.To the best of these authors’knowledge,this study is the first to calculate the deceptive efficiency and functional continuity of the MTD against drones and to normalize the trade-off according to a sensitivity analysis with the optimum. 展开更多
关键词 Moving-target-defense(MTD) DRONE formal methods game theory
下载PDF
Hierarchical Controller Synthesis Under Linear Temporal Logic Specifications Using Dynamic Quantization
5
作者 Wei Ren Zhuo-Rui Pan +1 位作者 Weiguo Xia Xi-Ming Sun 《IEEE/CAA Journal of Automatica Sinica》 SCIE EI CSCD 2024年第10期2082-2098,共17页
Linear temporal logic(LTL)is an intuitive and expressive language to specify complex control tasks,and how to design an efficient control strategy for LTL specification is still a challenge.In this paper,we implement ... Linear temporal logic(LTL)is an intuitive and expressive language to specify complex control tasks,and how to design an efficient control strategy for LTL specification is still a challenge.In this paper,we implement the dynamic quantization technique to propose a novel hierarchical control strategy for nonlinear control systems under LTL specifications.Based on the regions of interest involved in the LTL formula,an accepting path is derived first to provide a high-level solution for the controller synthesis problem.Second,we develop a dynamic quantization based approach to verify the realization of the accepting path.The realization verification results in the necessity of the controller design and a sequence of quantization regions for the controller design.Third,the techniques of dynamic quantization and abstraction-based control are combined together to establish the local-to-global control strategy.Both abstraction construction and controller design are local and dynamic,thereby resulting in the potential reduction of the computational complexity.Since each quantization region can be considered locally and individually,the proposed hierarchical mechanism is more efficient and can solve much larger problems than many existing methods.Finally,the proposed control strategy is illustrated via two examples from the path planning and tracking problems of mobile robots. 展开更多
关键词 Abstraction-based control design dynamic quantization formal methods linear temporal logic(LTL)
下载PDF
Formal analysis of robust email protocol based on authentication tests 被引量:1
6
作者 蒋睿 胡爱群 《Journal of Southeast University(English Edition)》 EI CAS 2009年第2期147-151,共5页
Based on the authentication tests and the strand space model, the robust email protocol with perfect forward secrecy is formally analyzed, and the security shortcomings of the protocol is pointed out. Meanwhile, the m... Based on the authentication tests and the strand space model, the robust email protocol with perfect forward secrecy is formally analyzed, and the security shortcomings of the protocol is pointed out. Meanwhile, the man-in-the-middle attack to the protocol is given, where the attacker forges the messages in the receiving phase to cheat the two communication parties and makes them share the wrong session keys with him. Therefore, the protocol is not ensured to provide perfect forward secrecy. In order to overcome the above security shortcomings, an advanced email protocol is proposed, where the corresponding signatures in the receiving phase of the protocol are added to overcome the man-in-the-middle attack and ensure to provide perfect forward secrecy. Finally, the proposed advanced email protocol is formally analyzed with the authentication tests and the strand space model, and it is proved to be secure in authentication of the email sender, the recipient and the server. Therefore, the proposed advanced email protocol can really provide perfect forward secrecy. 展开更多
关键词 email protocol authentication tests formal method perfect forward secrecy strand space model
下载PDF
A Formal Reputation System for Trusting Wireless Sensor Network 被引量:1
7
作者 XIAO Deqin FENG Jianzhao ZHANG Huanguo 《Wuhan University Journal of Natural Sciences》 CAS 2008年第2期173-179,共7页
In this paper, a formal system is proposed based on beta reputation for the development of trustworthy wireless sensor networks (FRS-TWSN). Following this approach, key concepts related to reputation are formal desc... In this paper, a formal system is proposed based on beta reputation for the development of trustworthy wireless sensor networks (FRS-TWSN). Following this approach, key concepts related to reputation are formal described step by step for wireless sensor networks where sensor nodes maintain reputation for other sensors and use it to evaluate their trustworthiness. By proving some properties of beta reputation system, the beta distribution is founded to fit well to describe reputation system. Also, a case system is developed within this framework for reputation representation, updates and integration. Simulation results show this scheme not only can keep stable reputation but also can prevent the system from some attacks as bad mouthing and reputation cheating. 展开更多
关键词 wireless sensor networks formal method REPUTATION Beta distribution
下载PDF
Formal Protection Architecture for Cloud Computing System 被引量:1
8
作者 Yasha Chen Jianpeng Zhao +1 位作者 Junmao Zhu Fei Yan 《ZTE Communications》 2014年第2期63-66,共4页
Cloud computing systems play a vital role in national security. This paper describes a conceptual framework called dualsystem architecture for protecting computing environments. While attempting to be logical and rigo... Cloud computing systems play a vital role in national security. This paper describes a conceptual framework called dualsystem architecture for protecting computing environments. While attempting to be logical and rigorous, formalism method is avoided and this paper chooses algebra Communication Sequential Process. 展开更多
关键词 formal method trusted computing PRIVACY cloud computing
下载PDF
Graphical Transformation of OWL Ontologies to Event-B Formal Models
9
作者 Eman H.Alkhammash 《Computers, Materials & Continua》 SCIE EI 2022年第2期3733-3750,共18页
Formal methods use mathematical models to develop systems.Ontologies are formal specifications that provide reusable domain knowledge representations.Ontologies have been successfully used in several data-driven appli... Formal methods use mathematical models to develop systems.Ontologies are formal specifications that provide reusable domain knowledge representations.Ontologies have been successfully used in several data-driven applications,including data analysis.However,the creation of formal models from informal requirements demands skill and effort.Ambiguity,inconsistency,imprecision,and incompleteness are major problems in informal requirements.To solve these problems,it is necessary to have methods and approaches for supporting the mapping of requirements to formal specifications.The purpose of this paper is to present an approach that addresses this challenge by using theWeb Ontology Language(OWL)to construct Event-B formal models and support data analysis.Our approach reduces the burden of working with the formal notations of OWL ontologies and Event-B models and aims to analyze domain knowledge and construct Event-B models from OWL ontologies using visual diagrams.The idea is based on the transformation of OntoGraf diagrams of OWL ontologies to UML-B diagrams for the purpose of bridging the gap between OWL ontologies and Event-B models.Visual data exploration assists with both data analysis and the development of Event-B formal models.To manage complexity,Event-B supports stepwise refinement to allow each requirement to be introduced at themost appropriate stage in the development process.UML-B supports refinement,so we also introduce an approach that allows us to divide and layer OntoGraf diagrams. 展开更多
关键词 Data analysis OWL ontologies event-B formal method REFINEMENT requirements OntoGraf
下载PDF
A Hybrid Formal Description Method Based on FSM,CSP and ADT for Communication Protocol
10
作者 Li Layman(Wuhan Transportation Universityl 430063, P. R. China) 《Journal of Systems Engineering and Electronics》 SCIE EI CSCD 1998年第3期29-38,共10页
Since communication protocol deals with complex issues related to distribution such as communication, concurrency and synchronization, their development needs to be traced by using sophisticated formal description met... Since communication protocol deals with complex issues related to distribution such as communication, concurrency and synchronization, their development needs to be traced by using sophisticated formal description methods. This paper presents a new hybrid formal method for communication protocol specification. In this method, finite state machine (FSM), communication sequential process (CSP) and abstract data type (ADT) are mixed and the best features of these approaches are offered. In this paper, the main formal description techniques (FDT) for protocol engineering are brieny introduced and a hybrid formal description method based on the FSM, CSP and ADT for communication protocol is described. Finally, this paper presents the formal specification of an example protocol for LAN by using the proposed hybrid formal method. The results of studies show that the hybrid formal description method for communication protocol is an available and effective approach. 展开更多
关键词 Communication protocol formal description techniques Protocol engineering Hybrid formal method
下载PDF
Model Checking Electronic CommerceSecurity Protocols Based on CTL 被引量:1
11
作者 XIAODe-qin ZHANGHuan-guo 《Wuhan University Journal of Natural Sciences》 EI CAS 2005年第1期333-337,共5页
We present a model based on Computational Temporal Logic (CTL) methods forverifying security requirements of electronic commerce, protocols. The model describes formally theauthentication, confidentiality integrity, n... We present a model based on Computational Temporal Logic (CTL) methods forverifying security requirements of electronic commerce, protocols. The model describes formally theauthentication, confidentiality integrity, non-repudiation) denial of serviee and access control ofthe e-lectronic commerce protocols. We illustrate as case study a variant of the Lu-Smolka protocolproposed by Lu-Smolka Moreover, we have discovered two attacks that allow a dishonest user topurchase a good debiting the amountto another user. And also, we compared our work with relativeresearch works and found lhat the formal way of this paper is more general to specify securityprotocols for E-Commerce. 展开更多
关键词 E-commercc security protocols formal methods computational temporal logic
下载PDF
Functional safety verification and performance measurement of train-train communication link
12
作者 LIN Junting XU Qian CHEN Yong 《Journal of Measurement Science and Instrumentation》 CAS CSCD 2021年第4期463-471,共9页
The short-range wireless communication technology has advanced considerably and provides the feasibility of train-train(T2T)communication link in the communication-based train control system.The introduction of the T2... The short-range wireless communication technology has advanced considerably and provides the feasibility of train-train(T2T)communication link in the communication-based train control system.The introduction of the T2T link would reduce the headway and improve operational efficiency.Formal methods are system design techniques that use rigorously specified mathematical models to ensure all behaviors work as expected.And it is exactly the functional safety verification needed.Therefore,to deal with the functional safety verification of the T2T link,an untimed colored petri net model is first constructed.Secondly,the verification process is performed.Conclusions can be drawn from the state space report and the computation tree logic queries.Lastly,the model is parameterized,and then data log files are obtained for further performance measurement.Results show that the proposed criteria are satisfied and there are no defects in the basic design requirements.The transmission delay has considered the reconnection,transmission errors and the interruption.The probability of the delay lower than 150 ms accounts for 98.106%,which meets the specification and the previous field test. 展开更多
关键词 functional safety formal methods colored Petri net(CPN) state space analysis performance measurement
下载PDF
A Comparative Typological Study of Italian and Georgian Jargon Words
13
作者 Nikoloz Esakia 《Sino-US English Teaching》 2022年第6期220-229,共10页
Italian youth speak their own language.The language used by youth can be considered a special language.Italian youth language has different functions.The functions which should be distinguished are:entertainment,expre... Italian youth speak their own language.The language used by youth can be considered a special language.Italian youth language has different functions.The functions which should be distinguished are:entertainment,expression,identity,and secrecy.Today,jargon has the function of entertainment more than that of secrecy.In Georgia,jargon has always been considered a foul and vulgar language.Georgian jargon words are less common than Italian ones.Georgian jargon has become popular recently.The material reviewed in the paper includes 2,700 items taken from dictionaries and the Internet.We divided them into two thematic groups:(1)related to everyday life;and(2)related to vicious aspects of life.The first group includes topics,such as money,work,the police,and youth discourse.The second group includes theft,drugs,sex life,and alcohol.The aim of this paper is to conduct a comparative study of groups of jargon identified as a result of thematic classification,in terms of methods of word formation.The study will allow us to identify semantic and formal methods of jargon word formation applied in these two unrelated languages,as well as similarities and differences between Italian and Georgian jargon words and phraseological units. 展开更多
关键词 youth language JARGON thematic classification semantic and formal methods word formation
下载PDF
A Privilege Separation Method for Security Commercial Transactions 被引量:1
14
作者 Chen Yasha Hu Jun +1 位作者 Sun Yu Gai Xinmao 《China Communications》 SCIE CSCD 2010年第6期94-99,共6页
Privilege user is needed to manage the commercial transactions, but a super-administrator may have monopolize power and cause serious security problem. Relied on trusted computing technology, a privilege separation me... Privilege user is needed to manage the commercial transactions, but a super-administrator may have monopolize power and cause serious security problem. Relied on trusted computing technology, a privilege separation method is proposed to satisfy the security management requirement for information systems. It authorizes the system privilege to three different managers, and none of it can be interfered by others. Process algebra Communication Sequential Processes is used to model the three powers mechanism, and safety effect is analyzed and compared. 展开更多
关键词 privilege separation fraud management security commercial transactions formal method
下载PDF
Survey of Smart Contract Technology and Application Based on Blockchain 被引量:2
15
作者 Somboun Tern 《Open Journal of Applied Sciences》 2021年第10期1135-1148,共14页
With the vigorous development of blockchain technology represented by</span><span style="font-family:""> Bitcoin, blockchain technology has gradually surpassed the era of programmable curren... With the vigorous development of blockchain technology represented by</span><span style="font-family:""> Bitcoin, blockchain technology has gradually surpassed the era of programmable currency and entered the era of smart contracts. Smart contracts are event-</span><span style="font-family:""> </span><span style="font-family:"">driven and stateful. With the in-depth development of blockchain technology, smart contracts use protocols and user interfaces to complete all steps of the contract process, allowing users to implement personalized code logic on the blockchain. Contract technology has the characteristics of decentralization, autonomy, observability, verifiability, and information sharing. It can effectively build programmable finance and programmable society, and is widely <span>used in digital payment, financial asset disposal, multi-signature contracts,</span> cloud computing, Internet of Things, sharing economy and other fields. First, it ex<span>plains the basic concepts, full life cycle, basic classification, basic structure, </span>key <span>technologies, development status and main technology platforms of smart</span> contracts;then discusses the application scenarios and development issues of smart contract technology, aiming to provide smart contract technology</span><span style="font-family:"">.</span><span style="font-family:""> The research and development provides reference. 展开更多
关键词 Smart Contract Blockchain Distributed Application formal Method Crowdsale Contract
下载PDF
Self Fault-Tolerance of Protocols: A Case Study
16
作者 Li, Layuan Li, Chunlin 《Journal of Systems Engineering and Electronics》 SCIE EI CSCD 2000年第3期28-34,共7页
The prerequisite for the existing protocols' correctness is that protocols can be normally operated under the normal conditions, rather than dealing with abnormal conditions. In other words, protocols with the fau... The prerequisite for the existing protocols' correctness is that protocols can be normally operated under the normal conditions, rather than dealing with abnormal conditions. In other words, protocols with the fault-tolerance can not be provided when some fault occurs. This paper discusses the self fault-tolerance of protocols. It describes some concepts and methods for achieving self fault-tolerance of protocols. Meanwhile, it provides a case study, investigates a typical protocol that does not satisfy the self fault-tolerance, and gives a new redesign version of this existing protocol using the proposed approach. 展开更多
关键词 Protocols Self fault-tolerance formal method Multimedia communications Protocol engineering.
下载PDF
The specification and analysis of network embedded system
17
作者 张冠华 张连华 白英彩 《Journal of Harbin Institute of Technology(New Series)》 EI CAS 2005年第4期434-439,共6页
This paper proposes a formal method which is used to model and analyze network devices such as touters. It is based on an algebraic process called “ACSR-VP”, which enhances the original CCS algebraic process by inco... This paper proposes a formal method which is used to model and analyze network devices such as touters. It is based on an algebraic process called “ACSR-VP”, which enhances the original CCS algebraic process by incorporating the notions of time, resource requirements, dynamic prioritization, and synchronization. Therefore, although there are many formal methods to analyze the timed concurrency system, ACSR-VP, due to its prominent features, is best fit for analysis of a resource bounded real-time system. This paper extends ACSR-VP to EACSR-VP, which is more adaptive to the features of network devices and specializes in analyzing this kind of embedded system. EACSR-VP adds the notion of n-way communication which allows more than two processes to participate in synchronization. It also enhances value-passing capabilities which make for more flexible specifications. Finally, specifications, verification and analysis methods with EACSR-VP are introduced by a case study of router with multiple input queues. 展开更多
关键词 formal method process algebra network devices MODELING
下载PDF
Research and improvement on the limitation of authentication test
18
作者 刘家芬 Zhou Mingtian 《High Technology Letters》 EI CAS 2008年第3期266-270,共5页
This paper elaborated on the limitation of authentication test theorem, illustrated the fundamental cause of that limitation through examples, then enhanced authentication test to solve this problem, and also proved t... This paper elaborated on the limitation of authentication test theorem, illustrated the fundamental cause of that limitation through examples, then enhanced authentication test to solve this problem, and also proved the soundness of that improvement with formal method. The enhanced theory can deal with protocols with test component as proper subterm of other regular node' s component under certain conditions, and extend the application scope of authentication test. With enhanced authentication test, the automatic protocol verification tools will be more efficient and convenient. 展开更多
关键词 authentication test strand space formal method security protocol analysis
下载PDF
Infinitely Many Symmetries of Konopelchenko-Dubrovsky Equation
19
作者 LI Zhi-Fang RUAN Hang-Yu 《Communications in Theoretical Physics》 SCIE CAS CSCD 2005年第3X期385-388,共4页
A set of generalized symmetries with arbitrary functions of t for the Konopelchenko-Dubrovsky (KD)equation in 2+1 space dimensions is given by using a direct method called formal function series method presented by Lo... A set of generalized symmetries with arbitrary functions of t for the Konopelchenko-Dubrovsky (KD)equation in 2+1 space dimensions is given by using a direct method called formal function series method presented by Lou. These symmetries constitute an infinite-dimensional generalized w∞ algebra. 展开更多
关键词 formal function series method Konopelchenko-Dubrovsky equation infinite dimensional generalized ω∞ algebra
下载PDF
Specification and Verification of Dynamically Reconfigurable Systems Using Dynamic Linear Hybrid Automata
20
作者 Ryo Yanase Tatsunori Sakai +1 位作者 Makoto Sakai Satoshi Yamane 《Journal of Software Engineering and Applications》 2016年第9期452-478,共27页
A dynamically reconfigurable system can change its configuration during operation, and studies of such systems are being carried out in many fields. In particular, medical technology and aerospace engineering must ens... A dynamically reconfigurable system can change its configuration during operation, and studies of such systems are being carried out in many fields. In particular, medical technology and aerospace engineering must ensure system safety because any defect will have serious consequences. Model checking is a method for verifying system safety. In this paper, we propose the Dynamic Linear Hybrid Automaton (DLHA) specification language and show a method to analyze reachability for a system consisting of several DLHAs. 展开更多
关键词 formal Method Model Checking Hybrid Automata Embedded Systems Dynamically Reconfigurable Systems
下载PDF
上一页 1 2 下一页 到第
使用帮助 返回顶部