Integrating object-oriented methods and formal methods for requirement engineering

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 for Commercial Applications Issues vs. Solutions

It was advocated that in 21st century, most of software will be developed with benefits of formal methods. The benefits include faults found in earlier stage of software development, automating, checking the certain properties and minimizing rework. In spite of their recognition in academic world and these claimed advantages, formal methods are still not widely used by commercial software industry. The purpose of this research is to promote formal methods for commercial software industry. In this paper we have identified issues in use of formal methods for commercial applications and devised strategies to overcome these difficulties which will provide motivations to use formal methods for commercial applications.

Integrating Formal Methods in XP—A Conceptual Solution

Formal methods can be used at any stage of product development process to improve the software quality and efficiency using mathematical models for analysis and verification. From last decade, researchers and practitioners are trying to establish successful transfer of practices of formal methods into industrial process development. In the last couple of years, numerous analysis approaches and formal methods have been applied in different settings to improve software quality. In today’s highly competitive software development industry, companies are striving to deliver fast with low cost and improve quality solutions and agile methodologies have proved their efficiency in acquiring these. Here, we will present an integration of formal methods, specifications and verification practices in the most renowned process development methodology of agile i.e. extreme programming with a conceptual solution. That leads towards the development of a complete formalized XP process in future. This will help the practitioners to understand the effectiveness of formal methods using in agile methods that can be helpful in utilizing the benefits of formal methods in industry.

PLC Modeling and Checking Based on Formal Method

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

Why Formal Methods Are Considered for Safety Critical Systems?

Formal methods are the mathematically techniques and tools which are used at early stages of software development lifecycle processes. The utter need of using formal methods in safety critical system leads to accuracy, consistency and correctness in proposed system. In safety critical real time application, requirements should be unambiguous and very accurate which can be achieved by using mathematical theorems. There is utter need to focus on the requirement phase which is the most critical phase of SDLC. This paper focuses on the use of Z notation for incorporating the accuracy, consistency, and eliminates ambiguity in safety critical system: Road Traffic Management System as a case study. The syntax, semantics, type checking and domain checking are further verified by using Z/EVES: a Z notation type checker tool.

Systematic Method for Constructing Lewis Representations

The systematic method for constructing Lewis representations is a method for representing chemical bonds between atoms in a molecule. It uses symbols to represent the valence electrons of the atoms involved in the bond. Using a number of rules in a defined order, it is often better suited to complicated cases than the Lewis representation of atoms. This method allows us to determine the formal charge and oxidation number of each atom in the edifice more efficiently than other methods.

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.

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.

A Hybrid Formal Description Method Based on FSM,CSP and ADT for Communication Protocol

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.

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.

Formal Derivation of the Combinatorics Problems with PAR Method

Partition-and-Recur (PAR) method is a simple and useful formal method. It can be used to design and testify algo-rithmic programs. In this paper, we propose that PAR method is an effective formal method on solving combinatorics problems. Furthermore, we formally derive combinatorics problems by PAR method, which cannot only simplify the process of algorithmic program's designing, but also improve its automatization, standardization and correctness. We develop algorithms for two typical combinatorics problems, the number of string scheme and the number of error per-mutation scheme. Lastly, we obtain accurate C++ programs which are transformed by automatic transforming system of PAR platform.

基于递归认证测试的SIP协议形式化分析

文章以形式化分析方法证明协议安全为研究目的,以具有灵活性、开放性、可伸缩性等特性的SIP协议为研究对象,运用基于串空间理论改进的递归认证测试形式化分析方法,分析了一种BAN逻辑证明安全的SIP身份认证协商协议,发现了该协议执行过程中协议格式不准确、易受中间人攻击的缺陷,并提出了针对该协议缺陷的改进方案。结果表明,文章所提出的递归认证测试形式化分析方法比BAN逻辑更适用、更有效,同时改进方案也增强了SIP身份认证协商协议的安全性。

Hierarchical Controller Synthesis Under Linear Temporal Logic Specifications Using Dynamic Quantization

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.

金融能力、正规信贷约束与农户创业行为

基于金融能力和正规信贷约束视角,利用2017年和2019年CHFS微观数据,通过构建Probit模型实证分析金融能力对农户创业行为的影响,探讨正规信贷约束在金融能力和农户创业行为关系中发挥的中介效应。结果表明:金融能力对农户创业行为具有显著正向影响,且在考虑内生性的情况下,该结论仍然成立;中介机制检验表明,金融能力能够通过缓解正规信贷约束来促进农户创业行为;异质性分析表明,中、西部地区和三线及以下城市的农户金融能力对其创业行为的影响更为显著。据此,建议建立完善的金融能力培养体系,加大对欠发达地区的政策扶持,且提高正规信贷支持力度。

基于MTRDL的自动飞行系统模式需求建模与验证方法

在民机自动飞行过程中,自动飞行系统模式转换是影响安全的重要因素,随着现代民机机载系统的功能与复杂度的快速增长,在需求阶段对自动飞行系统模式转换的安全性分析和验证成为重要的挑战.飞行模式转换的复杂性不仅体现在自动飞行过程中必需的多重飞行模式之间的交互关系,还体现在模式转换与外部环境之间复杂的数据与控制交联关系,这些交联关系同时隐含了飞行模式转换的安全性质,这些特征提高了形式化方法的应用难度.提出一种领域特定的建模验证框架:首先,提出面向自动飞行系统模式转换的领域需求建模语言MTRDL和基于该语言扩展于SysML上的建模方法;其次,提出基于安全需求模板的安全性质辅助规约方法;最后,通过对某机型的若干条目化需求的实例研究,证明所提方法在自动飞行系统模式转换需求验证中的有效性.

Formal analysis of robust email protocol based on authentication tests

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.

完备神经网络验证加速技术综述

人工智能技术已被广泛应用于生活中的各个领域.然而,神经网络作为人工智能的主要实现手段,在面对训练数据之外的输入或对抗攻击时,可能表现出意料之外的行为.在自动驾驶、智能医疗等安全攸关领域,这些未定义行为可能会对生命安全造成重大威胁.因此,使用完备验证方法证明神经网络的性质,保障其行为的正确性显得尤为重要.为了提高验证效率,各种完备神经网络验证工具均提出各自的优化方法,但并未充分探索这些方法真正起到的作用,后来的研究者难以从中找出最有效的优化方向.介绍神经网络验证领域的通用技术,并提出一个完备神经网络验证的通用框架.在此框架中,重点讨论目前最先进的工具在约束求解、分支选择与边界计算这3个核心部分上的所采用的优化方法.针对各个工具本身的性能和核心加速方法,设计一系列实验,旨在探究各种加速方式对于工具性能的贡献,并尝试寻找最有效的加速策略和更具潜力的优化方向,为研究者提供有价值的参考.

A Formal Reputation System for Trusting Wireless Sensor Network

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.

A Privilege Separation Method for Security Commercial Transactions

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.