On the use of formal methods to model and verify neuronal archetypes

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.

Formal methods, statistical debugging and exploratory analysis in support of system development: Towards a verification and validation calculator tool

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.

MF2-DMTD: A Formalism and Game-Based Reasoning Framework for Optimized Drone-Type Moving Target Defense

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.

Graphical Transformation of OWL Ontologies to Event-B Formal Models

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.

A Comparative Typological Study of Italian and Georgian Jargon Words

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.

Survey of Smart Contract Technology and Application Based on Blockchain

With the vigorous development of blockchain technology represented by Bitcoin, blockchain technology has gradually surpassed the era of programmable currency and entered the era of smart contracts. Smart contracts are event- 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 used in digital payment, financial asset disposal, multi-signature contracts, cloud computing, Internet of Things, sharing economy and other fields. First, it explains the basic concepts, full life cycle, basic classification, basic structure, key technologies, development status and main technology platforms of smart contracts;then discusses the application scenarios and development issues of smart contract technology, aiming to provide smart contract technology. The research and development provides reference.

Specification and Verification of Dynamically Reconfigurable Systems Using Dynamic Linear Hybrid Automata

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.

Binary Logic State Transition Oriented Formal General Reliability Model

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.

A Formal Method for Developing Algebraic and Numerical Algorithms

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.

Confidential computing and related technologies:a critical review

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.

Extension formulae on almost complex manifolds

We give the extension formulae on almost complex manifolds and give decompositions of the extension formulae.As applications,we study(n,0)-forms,the(n,0)-Dolbeault cohomology group and(n,q)-forms on almost complex manifolds.

Multi-agent system motion planning under temporal logic specifications and control barrier function

In this paper,w e provide a novel scheme to solve the motion planning problem of multi-agent systems under high-level task specifications.First,linear temporal logic is applied to express the global task specification.Then an efficient and decentralized algorithm is proposed to decom pose it into local tasks.M oreover,w e use control barrier function to synthesize the local controller for each agent under the linear temporal logic motion plan with safety constraint.Finally,simulation results show the effectiveness and efficiency of our proposed scheme.

Quantitative evaluation of model consistency evolution in compositional service-oriented simulation using a connected hyper-digraph

Appropriate maintenance technologies that facilitate model consistency in distributed simulation systems are relevant but generally unavailable.To resolve this problem,we analyze the main factors that cause model inconsistency.The analysis methods used for traditional distributed simulations are mostly empirical and qualitative,and disregard the dynamic characteristics of factor evolution in model operational running.Furthermore,distributed simulation applications(DSAs)are rapidly evolving in terms of large-scale,distributed,service-oriented,compositional,and dynamic features.Such developments present difficulty in the use of traditional analysis methods in DSAs,for the analysis of factorial effects on simulation models.To solve these problems,we construct a dynamic evolution mechanism of model consistency,called the connected model hyper-digraph(CMH).CMH is developed using formal methods that accurately specify the evolutional processes and activities of models(i.e.,self-evolution,interoperability,compositionality,and authenticity).We also develop an algorithm of model consistency evolution(AMCE)based on CMH to quantitatively and dynamically evaluate influencing factors.Experimental results demonstrate that non-combination(33.7%on average)is the most influential factor,non-single-directed understanding(26.6%)is the second most influential,and non-double-directed understanding(5.0%)is the least influential.Unlike previous analysis methods,AMCE provides good feasibility and effectiveness.This research can serve as guidance for designers of consistency maintenance technologies toward achieving a high level of consistency in future DSAs.