一种面向嵌入式软件体系结构的形式化建模方法

为了解决MARTE（Modeling and Analysis of Real Time and Embedded systems）在建立嵌入式软件模型时不够精确的问题,结合Object-Z和PTA（Probabilistic Timed Automation）的优点,本文提出了一种集成的形式化建模方法--PTA-OZ.该方法不仅能够对嵌入式软件模型的静态语义和动态语义进行精确描述,而且通过模型转换规则,能够将MARTE模型转换为PTA-OZ模型.并对模型转换的语义一致性进行了验证,证明本文方法在转换过程能够保持结构语义和行为语义的一致性.最后通过实例模型描述从嵌入式软件建模到属性检验的过程.     

一种安全协议的组合分析模型研究

 在当前安全协议形式化分析的研究中,亟待解决的关键问题是如何形式化描述更多的安全属性,如何将这些属性在统一的框架下进行形式化分析和验证.本文提出了一种统一的安全属性形式化描述方法,在此基础上,利用知识推理来弥补进程演算缺乏数据结构的固有缺陷,从而提出了一种安全协议形式化分析的一般组合模型.通过实例分析验证了模型的有效性,并指出了该模型的研究方向.     

状态不可观测的信息物理融合系统运行时验证

确保信息物理融合系统（Cyber-Physical System,CPS）运行时行为正确性是至关重要的,尤其在航空航天、汽车、核电和医疗等安全攸关领域.本文针对具有随机行为且状态不可观测的CPS,提出一种基于隐马尔科夫模型的运行时安全性验证方法.首先构造状态不可观测的CPS运行时安全性验证框架,该框架通过隐马尔科夫模型表示系统,使用确定性有限自动机规约系统安全属性的否定,两者的乘积自动机作为运行时监控器,从而将CPS运行时安全性验证问题约简到监控器上的概率推断问题.然后,提出一种增量迭代安全性验证算法以及反例生成算法.实验结果表明本文算法和粒子滤波算法相比预测错误率下降了近20%,并且当系统违背安全属性时,本文的方法能给出反例.     

基于CSP的多线程自动建模及死锁检测研究

并发模型分析主要用于业务流程逻辑验证,并不能很好支持多线程程序建模。目前大部分研究主要针对Java程序的死锁检测,对于使用POSIX线程库开发的C语言程序研究并不多。为了检测POSIX线程库开发的C语言程序是否存在死锁问题,提出一种对多线程程序进行自动建模与死锁检测的形式化验证方法。首先,根据C++CSP框架和源程序之间的联系,实现源程序到C++CSP框架的语义转换;然后,对C++CSP框架建立通信顺序进程(CSP)模型,并通过过程分析工具(PAT)对建立的模型进行死锁检测;最后,通过实例验证了本文中自动建模与死锁检测方法的可行性与有效性。     

移动代理完整性协议形式化分析方法研究

 本文给出了移动代理协议数据完整性属性的定义,指出了采用传统认证性属性来分析移动代理数据完整性属性的不足,从而给出了移动代理完整性证明的两个形式化规约:数据完整性规约和序列完整性规约.在此基础上,针对典型协议实例进行CPS建模,并采用阶函数的方法证明了其完整性,验证了完整性规约的正确性和有效性.     

可移动系统安全模型统一框架

本文的主要工作是利用可移动进程的形式化模型π演算为工具,考虑系统的移动性(Mobility),将系统安全属性的刻画归结为特定系统进程等价的验证,提出一种新的安全模型框架.在此框架下,可以方便表示不同的不干涉安全属性,并对其进行强弱对比;针对不同安全需求,可定义新的安全属性.并且,该框架建立一个新的安全属性研究的平台,可广泛地适用于具有移动进程的分布式系统的安全分析.     

信息物理融合系统软件可信性演化动力学建模

信息物理融合系统(CPS)软件可信性建模是CPS可信软件开发过程中至关重要的一环,现有的形式化方法、软件验证技术并不适合对CPS软件可信性动态演化进行描述和分析。在深入分析CPS可信软件动态演化过程的基础上,结合非线性动力学的基本理论和方法,研究CPS软件可信性演化的动力学机制,对CPS软件在内外双重因素影响下的可信性演化过程进行建模,并分析其可信性演化规律,为CPS软件可信性研究提供了一种新手段。通过对一个工业控制领域中CPS软件的建模与分析,验证了该方法的可行性。     

基于SmartVerif的比特币底层协议算力盗取漏洞发现

比特币引入了一种新的P2P(Peer to Peer)交易方法,并依靠其底层协议实现去中心化交易.然而,由于目前缺乏对比特币各底层协议的细粒度形式化分析和系统建模,比特币安全性并未被保证.本文通过设计多维度的比特币安全模型引理和细粒度的比特币模型规则,系统地抽象了多协议组合运行考虑下的比特币协议实体交互,完成了对比特币的形式化符号建模与自动化安全分析.与以前的工作相比,本文更细粒度地建模了比特币协议实体及其相关操作,并全面设计了满足比特币各实体需求的安全属性.此外,本文利用自动化形式化验证系统SmartVerif实现了无需额外手工推导证明的形式化验证实验,通过将本文所建模的符号模型规则与引理作为SmartVerif的输入,发现了比特币底层协议算力盗取攻击.     

从UML状态图到PVS规范的自动转换、验证

将UML(统一建模语言)图形转换成形式化规范是一种精确化UML语义、扩大形式化软件方法适用范围的有效途径.PVS是一种通用高阶逻辑形式化规范语言,具有很强的描述能力以及丰富的定理证明、模型验证工具支持.本文论证了使用.PVS来对UML进行形式化的优势,并且给出了UML的状态图到PVS规范的转换模型与规则.     

基于模型检测的UML状态图和顺序图一致性检测

用户可使用UML从不同角度对系统进行建模,但不同视图间存在信息冗余,会导致视图不一致的问题。文中提出形式化与可视化UML互补建模的方法,探讨用模型检测验证UML模型中的状态图和顺序图的一致性问题。针对具有复合片段的顺序图提出分析方法,将复杂层次结构的状态图转换为有限状态机,再用模型检测工具NuSMV对建立的模型进行验证。最后通过实例对此转换方法进行验证,实验结果表明了此方法的有效性。     

An automated parallel simulation flow for cyber-physical system design

Parallel and distributed simulation (PDS) is often employed to tackle the computational intensity of system-level simulation of real-world complex embedded and cyber-physical systems (CPSs). However, CPS models comprise heterogeneous components with diverge semantics for which incompatible PDS approaches are developed. We propose an automated PDS flow based on a formal modeling framework—with necessary extensions—targeting heterogeneous embedded and CPS design. The proposed flow characterizes the sequential executable specification of a heterogeneous model and generates a PDS cluster. State-of-the-art graph partitioning methods are adopted and a new extensible constraint-base formulation of the model partitioning problem is developed. The applicability, effectiveness, and scalability of the proposed flow is demonstrated using case studies.     

System of Systems Approach to Formal Modeling of CPS for Simulation‐Based Analysis

This paper presents a system‐of‐systems (SoS) approach to the formal modeling of a cyber‐physical system (CPS) for simulation‐based analysis. The approach is based on a convergence technology for modeling and simulation of a highly complex system in which SoS modeling methodology, hybrid systems modeling theory, and simulation interoperation technology are merged. The methodology maps each constituent system of a CPS to a disparate model of either continuous or discrete types. The theory employs two formalisms for modeling of the two model types with formal specification of interfaces between them. Finally, the technology adapts a simulation bus called DEVS BUS whose protocol synchronizes time and exchange messages between subsystems simulation. Benefits of the approach include reusability of simulation models and environments, and simulation‐based analysis of subsystems of a CPS in an inter‐relational manner.     

Security risk management in the BT HP alliance

This paper describes the way BT and HP have agreed to collaboratively manage security risks within the BT HP alliance. BT and HP have worked together to establish an environment of mutual trust. A rigorous alignment of policy, coupled with an effective governance framework, has enabled the development of an agreed risk assessment and mitigation process. This paper examines the way in which the foundations of mutual trust were developed and how these enabled the development of a federated security model. The challenge within any outsource arrangement is to determine how security risk assessment and management, built up through policy compliance and developed best practice in a single company in-house environment, should change when the responsibility for a significant part of the delivery and future development of service capability is transferred to a third party. The additional challenge to BT and HP was to ensure that the solution should be scalable and enduring in the context of a strategic alliance. The initial work of the security communities in the two companies was focused on the assessment and management of the risk associated with the managed service agreement to transfer the management responsibility from BT to HP for the mid-range server estate and the end-user workspace (or desktop). This managed service agreement was one of the three core agreements included within the strategic alliance agreement entered into by the two companies. There was a clear objective of ensuring applicability to the other work streams and scalability across all commercial activities of the BT HP alliance. The main focus of the work was to build on top of the technical capabilities of both companies to ensure that formal governance processes were put in place and that security risks were consistently measured, assessed and managed. The trust established between HP and BT as result of the adoption of a common risk assessment methodology and creation of a robust governance framework enabled a swift resolution of early issues concerning HP agent access to BT systems. A Security Federation model was established to facilitate the accreditation of users within their home domains, which delivered significant operational savings to both parties. The paper describes the value obtained from this approach with respect to security issues during the first twenty-four months of the BT HP alliance. HP     

基于时序关系的消息推理及安全协议符号迹分析

如何准确地描述敌意环境中的协议运行模型和在统一的框架下分析多种安全属性是安全协议形式化分析中的两个关键问题。提出了基于时序关系的消息推理,把实体的知识与协议的符号迹分析结合起来,构建了协议运行的一般模型。在此模型下,消息间的相互关系被用来统一多种安全属性的形式化表达,定义了相应的属性满足关系,提出了分析安全协议的一般框架。最后给出了一个实例分析,并指出该框架以后的研究方向。     

A Divergence Minimization Approach to Joint Multiuser Decoding for Coded CDMA

In this paper, a theoretical framework of divergence minimization (DM) is applied to derive iterative receiver algorithms for coded CDMA systems. The DM receiver obtained performs joint channel estimation, multiuser decoding, and noise- covariance estimation. While its structure is similar to that of many ad-hoc receivers in the literature, the DM receiver is the result of applying a formal framework for optimization without further simplifications, namely the DM approach with a factorizable auxiliary model distribution. The well-known expectation- maximization (EM) algorithm and space-alternating generalized expectation-maximization (SAGE) algorithm are special cases of degenerate model distributions within the DM framework. Furthermore, many ad-hoc receiver structures from literature are shown to represent approximations of the proposed DM receiver. The DM receiver has four interesting properties that all result directly from applying the formal framework: (i) The covariances of all estimates involved are taken into account, (ii) The residual interference after interference cancellation is handled by the noise-covariance estimation as opposed to by LMMSE filters in other receivers, (iii) Posterior probabilities of the code symbols are employed rather than extrinsic probabilities, (iv) The iterative receiver is guaranteed to converge in divergence. The theoretical insights are illustrated by simulation results.     

Business Process Modelling and Design — A Formal Model and Methodology

This paper presents a formal framework for representing enterprise knowledge. The concepts of our framework (objectives and goals, roles and actors, actions and processes, responsibilities and constraints) allow business analysts to capture knowledge about an enterprise in a way that is both intuitive and mathematically formal. It also outlines the basic steps of a methodology that allows business analysts to go from high-level enterprise objectives, to detailed and formal specifications of business processes that can be enacted to realise these objectives. The formal language used means that the specifications can be verified as having certain correctness properties, e.g. that responsibilities assigned to roles are fulfilled, and constraints are maintained as a result of process execution.     

A secure end‐to‐end SMS‐based mobile banking protocol

Short message service (SMS) provides a wide channel of communication for banking in mobile commerce and mobile payment. The transmission of SMS is not secure in the network using global system for mobile communications or general packet radio service. Security threats in SMS restricted the use of SMS in mobile banking within certain limits. This paper proposed a model to address the security of SMS using elliptic curve cryptography. The proposed model provides end‐to‐end SMS communication between the customer and the bank through the mobile application. The main objective of the proposed model is to design and develop a security framework for SMS banking. Further, the protocol is verified for its correctness and security properties because most of the protocols are not having the facility to be verified by using the formal methods. Our proposed framework is experimentally validated by formal methods using model checking tool called automated validation of internet security protocols and Scyther tools. Security analysis shows that the proposed mechanism works better compared to existing SMS payment protocols for real‐world applications.     

Registration of image feature points using differential evolution

Registrationoffeaturepointsisacommonproblemof imageregistration[1,2].Theproblemaddressedinthispaperistosearchfortheoptimaltransformationthat makesthebestalignmentoftwofeaturepointsetswith outcorrespondences.Theregistrationofpointsetscanbeformulatedintermsofglobaloptimizationwhicha voidsbothlocalentrapmentandexhaustivesearch.In theframeworkofoptimization,theobjectivefunctiontobeminimizedisusuallymappedtothesimilaritybe tweenthepointsets,whilethefunctionalvariablesare thetransformationparamet…