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.展开更多
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.展开更多
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.展开更多
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.展开更多
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 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.展开更多
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.展开更多
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.展开更多
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.展开更多
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.展开更多
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.展开更多
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.展开更多
This paper presents the formal specification and model-checklng of Carrier Sense Multiple Access with Collision Avoidance( CSMA/CA) protocol using the model checker we developed for real-time systems, which are spec...This paper presents the formal specification and model-checklng of Carrier Sense Multiple Access with Collision Avoidance( CSMA/CA) protocol using the model checker we developed for real-time systems, which are specified as networks of finite precision timed automata. The CSMA/CA protocol proposed in the IEEE 802.11 standard is designed to reduce the probability of collision during a transmission in wireless random access environments. However, it does not eliminate completely the possibility of a collision between two or more frames transmitted simultaneously. We investigate what will give rise to a collision between frames and use our automatic verification tool for model-checking.展开更多
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.展开更多
Ensuring the correctness and reliability of large-scale resource sharing and complex job processing Is an Important task for grid applications. From a formal method perspective, a grid service chain model based on sta...Ensuring the correctness and reliability of large-scale resource sharing and complex job processing Is an Important task for grid applications. From a formal method perspective, a grid service chain model based on state PI calculus Is proposed In this work as the theoretical foundation for the service composition and collaboration in grid. Following the Idea of the Web Service Resource Framework (WSRF), state PI calculus enables the life-cycle management of system states by associating the actions in the original PI calculus with system states. Moreover, model checking technique is exploltad for the design-time and run-time logical verification of grid service chain models. A grid application scenario of the dynamic analysis of material deformation structure is also provided to show the effectiveness of the proposed work.展开更多
There were various conventional modeling techniques with varied semantics for system reliability assessment, such as fault trees(FT), Markov process(MP), and Petri nets. However, it is strenuous to construct and to ma...There were various conventional modeling techniques with varied semantics for system reliability assessment, such as fault trees(FT), Markov process(MP), and Petri nets. However, it is strenuous to construct and to maintain models utilizing these formalisms throughout the life cycle of system under development. This paper proposes a unified formal modeling language to build a general reliability model. The method eliminates the gap between the actual system and reliability model and shows details of the system clearly. Furthermore,the model could be transformed into FT and MP through specific rules defined by a formal language to assess system-level reliability.展开更多
The development of algebraic and numerical algorithms is a kind of complicated creative work and it is difficult to guarantee the correctness of the algorithms. This paper introduces a systematic and unified formal de...The development of algebraic and numerical algorithms is a kind of complicated creative work and it is difficult to guarantee the correctness of the algorithms. This paper introduces a systematic and unified formal development method of algebraic and numerical algorithms. The method implements the complete refinement process from abstract specifications to a concrete executable program. It uses the core idea of partition and recursion for formal derivation and combines the mathematical induction based on strict mathematical logic with Hoare axiom for correctness verification. This development method converts creative work into non-creative work as much as possible while ensuring the correctness of the algorithm, which can not only verify the correctness of the existing algebraic and numerical algorithms but also guide the development of efficient unknown algorithms for such problems. This paper takes the non-recursive implementation of the Extended Euclidean Algorithm and Horner's method as examples. Therefore, the effectiveness and feasibility of this method are further verified.展开更多
Probabilistic techniques are widely used in the analysis of algorithms to estimate the computational complexity of algorithms or a computational problem.Traditionally,such analyses are performed using paper-and-pencil...Probabilistic techniques are widely used in the analysis of algorithms to estimate the computational complexity of algorithms or a computational problem.Traditionally,such analyses are performed using paper-and-pencil proofs and the results are sometimes validated using simulation techniques.These techniques are informal and thus may result in an inaccurate analysis.In this paper,we propose a formal technique for analyzing the expected time complexity of algorithms using higher-order-logic theorem proving.The approach calls for mathematically modeling the algorithm along with its inputs,using indicator random variables,in higher-order logic.This model is then used to formally reason about the expected time complexity of the underlying algorithm in a theorem prover.The paper includes the higher-order-logic formalization of indicator random variables,which are fundamental to the proposed infrastructure.In order to illustrate the practical effiectiveness and utilization of the proposed infrastructure,the paper also includes the analysis of algorithms for three well-known problems,i.e.,the hat-check problem,the birthday paradox and the hiring problem.展开更多
The advantage of COOZ (Complete Object-Oriented Z) is to specify large scale software, but it does not support refinement calculus. Thus its application is confined for software development. Including refinement calc...The advantage of COOZ (Complete Object-Oriented Z) is to specify large scale software, but it does not support refinement calculus. Thus its application is confined for software development. Including refinement calculus into COOZ overcomes its disadvantage during design and implementation. The separation between the design and implementation for structure and notation is removed as well. Then the software can be developed smoothly in the same frame. The combina- tion of COOZ and refinement calculus call build object-oriented frame, in which the specification in COOZ is refined stepwise to code by calculus. In this paper, the development model is established, which is based on COOZ and refinement calculus. Data refinement is harder to deal with in a refinement tool than ordinary algorithmic refinement, since data refinement usually has to be done on a large program component at once. As to the implemelltation technology of refinement calculus, the data refinement calculator is constructed and an approach for data refinement which is based on data refinement calculus and program window inference is offered.展开更多
This research critically reviews the definition of confidential computing(CC)and the security comparison of CC with other related technologies by the Confidential Computing Consortium(CCC).We demonstrate that the defi...This research critically reviews the definition of confidential computing(CC)and the security comparison of CC with other related technologies by the Confidential Computing Consortium(CCC).We demonstrate that the definitions by CCC are ambiguous,incomplete and even conflicting.We also demonstrate that the security comparison of CC with other technologies is neither scientific nor fair.We highlight the issues in the definitions and comparisons and provide initial recommendations for fixing the issues.These recommendations are the first step towards more precise definitions and reliable comparisons in the future.展开更多
基金This work was supported by the French government through the UCA-Jedi project managed by the National Research Agency(ANR-15-IDEX-01)in particular,by the interdisciplinary Institute for Modeling in Neuroscience and Cognition(NeuroMod)of the UniversitéCôte d'Azur.It was also supported by the Natural Sciences and Engineering Research Council of Canada.
文摘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.
文摘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.
基金funding by the Challengeable Future Defense Technology Research and Development Program through the Agency For Defense Development(ADD)funded by the Defense Acquisition Program Administration(DAPA)in 2023(No.915024201).
文摘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.
基金the National Natural Science Foundation of China (60573043)the Natural Science Foundation of Guangdong Province (06025838)
文摘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.
文摘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.
基金This work was supported by Taif University Researchers Supporting Project Number(TURSP-2020/292),Taif University,Taif,Saudi Arabia.
文摘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.
文摘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.
基金Supported by the Natural Science Foundation ofthe Department of Education of Guangdong Province (Z03001)
文摘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.
文摘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.
文摘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.
基金This project was supported by the National Natural Science Foundation of China and the Natural Science Foundation of Hubei Prov
文摘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.
文摘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.
基金The workreportedinthis paperissupported bythe National Grand Fundamental Research973 Programof China (2002cb312200) ,andthe National Nat-ural Science Foundation of China(60242002 ,60273025)
文摘This paper presents the formal specification and model-checklng of Carrier Sense Multiple Access with Collision Avoidance( CSMA/CA) protocol using the model checker we developed for real-time systems, which are specified as networks of finite precision timed automata. The CSMA/CA protocol proposed in the IEEE 802.11 standard is designed to reduce the probability of collision during a transmission in wireless random access environments. However, it does not eliminate completely the possibility of a collision between two or more frames transmitted simultaneously. We investigate what will give rise to a collision between frames and use our automatic verification tool for model-checking.
基金supported by the Fundamental Research Funds for the Central Universities(DUT22RT(3)090)the National Natural Science Foundation of China(61890920,61890921,62122016,08120003)Liaoning Science and Technology Program(2023JH2/101700361).
文摘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.
基金Supported by the National Natural Science Foundation of China (Grant Nos. 60604033 and 60553001)
文摘Ensuring the correctness and reliability of large-scale resource sharing and complex job processing Is an Important task for grid applications. From a formal method perspective, a grid service chain model based on state PI calculus Is proposed In this work as the theoretical foundation for the service composition and collaboration in grid. Following the Idea of the Web Service Resource Framework (WSRF), state PI calculus enables the life-cycle management of system states by associating the actions in the original PI calculus with system states. Moreover, model checking technique is exploltad for the design-time and run-time logical verification of grid service chain models. A grid application scenario of the dynamic analysis of material deformation structure is also provided to show the effectiveness of the proposed work.
文摘There were various conventional modeling techniques with varied semantics for system reliability assessment, such as fault trees(FT), Markov process(MP), and Petri nets. However, it is strenuous to construct and to maintain models utilizing these formalisms throughout the life cycle of system under development. This paper proposes a unified formal modeling language to build a general reliability model. The method eliminates the gap between the actual system and reliability model and shows details of the system clearly. Furthermore,the model could be transformed into FT and MP through specific rules defined by a formal language to assess system-level reliability.
基金Supported by the National Natural Science Foundation of China (61862033, 61762049, 61902162)Jiangxi Provincial Natural Science Foundation (20202BABL202026, 20202BABL202025, 20202BAB202015)。
文摘The development of algebraic and numerical algorithms is a kind of complicated creative work and it is difficult to guarantee the correctness of the algorithms. This paper introduces a systematic and unified formal development method of algebraic and numerical algorithms. The method implements the complete refinement process from abstract specifications to a concrete executable program. It uses the core idea of partition and recursion for formal derivation and combines the mathematical induction based on strict mathematical logic with Hoare axiom for correctness verification. This development method converts creative work into non-creative work as much as possible while ensuring the correctness of the algorithm, which can not only verify the correctness of the existing algebraic and numerical algorithms but also guide the development of efficient unknown algorithms for such problems. This paper takes the non-recursive implementation of the Extended Euclidean Algorithm and Horner's method as examples. Therefore, the effectiveness and feasibility of this method are further verified.
文摘Probabilistic techniques are widely used in the analysis of algorithms to estimate the computational complexity of algorithms or a computational problem.Traditionally,such analyses are performed using paper-and-pencil proofs and the results are sometimes validated using simulation techniques.These techniques are informal and thus may result in an inaccurate analysis.In this paper,we propose a formal technique for analyzing the expected time complexity of algorithms using higher-order-logic theorem proving.The approach calls for mathematically modeling the algorithm along with its inputs,using indicator random variables,in higher-order logic.This model is then used to formally reason about the expected time complexity of the underlying algorithm in a theorem prover.The paper includes the higher-order-logic formalization of indicator random variables,which are fundamental to the proposed infrastructure.In order to illustrate the practical effiectiveness and utilization of the proposed infrastructure,the paper also includes the analysis of algorithms for three well-known problems,i.e.,the hat-check problem,the birthday paradox and the hiring problem.
基金the National Natural Science Foundation of China (No.69673006) and theNational Ninth Five-Year Project (98-780-01-07-06) of Ch
文摘The advantage of COOZ (Complete Object-Oriented Z) is to specify large scale software, but it does not support refinement calculus. Thus its application is confined for software development. Including refinement calculus into COOZ overcomes its disadvantage during design and implementation. The separation between the design and implementation for structure and notation is removed as well. Then the software can be developed smoothly in the same frame. The combina- tion of COOZ and refinement calculus call build object-oriented frame, in which the specification in COOZ is refined stepwise to code by calculus. In this paper, the development model is established, which is based on COOZ and refinement calculus. Data refinement is harder to deal with in a refinement tool than ordinary algorithmic refinement, since data refinement usually has to be done on a large program component at once. As to the implemelltation technology of refinement calculus, the data refinement calculator is constructed and an approach for data refinement which is based on data refinement calculus and program window inference is offered.
基金Funded by DFG Grants 389792660 as part of TRR 248—CPECand 390696704 as part of CeTI.
文摘This research critically reviews the definition of confidential computing(CC)and the security comparison of CC with other related technologies by the Confidential Computing Consortium(CCC).We demonstrate that the definitions by CCC are ambiguous,incomplete and even conflicting.We also demonstrate that the security comparison of CC with other technologies is neither scientific nor fair.We highlight the issues in the definitions and comparisons and provide initial recommendations for fixing the issues.These recommendations are the first step towards more precise definitions and reliable comparisons in the future.