基于时间自动机的信息物理融合系统建模与验证

信息物理融合系统的建模和验证是当前研究的一个热点。本文通过分析信息物理融合系统的体系结构,利用时间自动机为建模工具,将该结构中的各个组件分别进行建模,以表现它们的分布性和实时性。这些时间自动机组成一个网络模型,用于刻划整个系统之间的并发通信和协作过程。最后,提出一组该系统要满足的性质(包括时间约束),运用模型检测工具UPPAAL自动验证本系统的正确性。     

A simplification of a real‐time verification problem

We revisit the problem of real‐time verification with dense‐time dynamics using timeout and calendar‐based models and simplify this to a finite state verification problem. We introduce a specification formalism for these models and capture their behaviour in terms of semantics of timed transition systems. We discuss a technique, which reduces the problem of verification of qualitative temporal properties on infinite state space of a large fragment of these timeout and calender‐based transition systems into that on clock‐less finite state models through a two‐step process comprising of digitization and finitary reduction. This technique enables us to verify safety invariants for real‐time systems using finite state model checking avoiding the complexity of infinite state (bounded) model checking and scale up models without applying techniques from induction‐based proof methodology. In the same manner, we verify timeliness properties. Moreover, we can verify liveness for real‐time systems, which are not possible by using induction with infinite state model checkers. Copyright © 2016 John Wiley & Sons, Ltd.     

基于UPPAAL的实时系统模型验证

UPPAAL是一种使用时间自动机模型的实时系统验证工具,它可以避免时间自动机求积时状态空间的爆炸。介绍了时间自动机理论和工具UPPAAL,着重说明如何用UPPAAL进行模型检查,并给出了一个应用实例。     

UPPAAL--一种适合自动验证实时系统的工具

UPPAAL是一个基于时间自动机的自动验证工具,已成功地用于实时控制器和通信协议等实时系统的验证.本文介绍了UPPAAL的语法,语义和语用,列举了它的几种扩展形式,并归纳了其应用及研究现状.     

Design and analysis of target‐sensitive real‐time systems

A significant number of real‐time control applications include computational activities where the results have to be delivered at precise instants, rather than within a deadline. The performance of such systems significantly degrades if outputs are generated before or after the desired target time. This work presents a general methodology that can be used to design and analyze target‐sensitive applications in which the timing parameters of the computational activities are tightly coupled with the physical characteristics of the system to be controlled. For the sake of clarity, the proposed methodology is illustrated through a sample case study used to show how to derive and verify real‐time constraints from the mission requirements. Software implementation issues necessary to map the computational activities into tasks running on a real‐time kernel are also discussed to identify the kernel mechanisms necessary to enforce timing constraints and analyze the feasibility of the application. A set of experiments are finally presented with the purpose of validating the proposed methodology. Copyright © 2015 John Wiley & Sons, Ltd.     

Multiprocessor platform for partitioned real‐time systems

Two current trends in the real‐time and embedded systems are the multiprocessor architectures and the partitioning technology that enables several isolated applications with different criticality levels to share the same computer. This paper presents a real‐time platform for multiprocessor and partitioned systems, in which communication requirements are also considered. The paper describes the adaptation of MaRTE OS (a monoprocessor real‐time operating system) to the XtratuM hypervisor for the multiprocessor Intel x86 architecture. This adaptation makes two contributions to ease the development process of future mixed‐criticality applications: firstly, it integrates the hypervisor technology and the fully partitioned scheduling in a multiprocessor environment, and secondly, it provides the basis to interconnect partitioned and non‐partitioned applications via a homogeneous communication subsystem. Copyright © 2016 John Wiley & Sons, Ltd.     

HARTEX—a safe real‐time kernel for distributed computer control systems

A hard real‐time kernel is presented for distributed computer control systems (DCCS), highlighting a number of novel features, such as integrated scheduling of hard and soft real‐time tasks as well as tasks and resources; high‐performance time management supporting safe DCCS operation in a hard real‐time environment; synchronization and communication featuring event notification via vector semaphores and transparent communication through implicit (content‐oriented) message addressing. Conventional queues have been substituted by Boolean vectors and vector processing techniques throughout the kernel, resulting in efficient and highly deterministic behaviour, which is characterized by very low overhead and constant execution time of kernel operations, independent of the number of tasks involved. Copyright © 2001 John Wiley & Sons, Ltd.     

Timing analysis of scenario‐based specifications using linear programming

Scenario‐based specifications (SBSs), such as UML interaction models, offer an intuitive and visual way of describing design requirements, and are playing an increasingly important role in the design of software systems. This paper presents an approach to timing analysis of SBSs expressed by UML interaction models. The approach considers more general and expressive timing constraints in UML sequence diagrams (SDs), and gives a solution to the reachability analysis, constraint conformance analysis and bounded delay analysis problems, which reduces these problems into linear programs. With the synchronous interpretation of the SD compositions, the timing analysis algorithms in the approach form a decision procedure for a class of SBSs where any loop in any path is time‐independent of the other parts in the path. These algorithms are also a semi‐decision procedure for general SBSs with both the synchronous and asynchronous composition semantics. The approach also supports bounded timing analysis of SBSs, which investigates all the paths in the bound limit one by one, and performs the timing analysis for each finite path by linear programming. A tool prototype has been developed to support this approach. Copyright © 2010 John Wiley & Sons, Ltd.     

Execution models for reconfigurable embedded real‐time systems

This paper deals with the verification and assignment into the execution environment of Reconfigurable Control Applications following the Component‐based International Industrial Standard IEC61499. According to this Standard, a Function Block (FB) is an event‐triggered component and an application is an FB network that has to meet temporal properties according to user requirements. If a reconfiguration scenario is applied at run‐time, then the FB network implementing the application is totally changed or modified. To cover all possible cases, we classify such scenarios into three classes and we define an agent‐based architecture designed with nested state machines to automatically handle all possible reconfigurations. To verify and assign Function Blocks corresponding to each reconfiguration scenario into the execution environment, we define an approach based on the exploration of reachability graphs to verify temporal properties. This approach constructs feasible Operating System tasks encoding the FB network that corresponds to each scenario. Therefore, the application is considered as sets of Operating System (OS) tasks where each set is to load in memory when the corresponding reconfiguration scenario is applied by the agent. We developed the tool X ‐Assign supporting these contributions that we apply on the FESTO production system available in our research laboratory. Copyright © 2009 John Wiley and Sons Asia Pte Ltd and Chinese Automatic Control Society     

Catching two rabbits: adaptive real‐time support for embedded Linux

The trend of digital convergence makes multitasking common in many digital electronic products. Some applications in those systems have inherent real‐time properties, while many others have few or no timeliness requirements. Therefore the embedded Linux kernels, which are widely used in those devices, provide real‐time features in many forms. However, providing real‐time scheduling usually induces throughput degradation in heavy multitasking due to the increased context switches. Usually the throughput degradation becomes a critical problem, since the performance of the embedded processors is generally limited for cost, design and energy efficiency reasons. This paper proposes schemes to lessen the throughput degradation, which is from real‐time scheduling, by suppressing unnecessary context switches and applying real‐time scheduling mechanisms only when it is necessary. Also the suggested schemes enable the complete priority inheritance protocol to prevent the well‐known priority inversion problem. We evaluated the effectiveness of our approach with open‐source benchmarks. By using the suggested schemes, the throughput is improved while the scheduling latency is kept same or better in comparison with the existing approaches. Copyright © 2008 John Wiley & Sons, Ltd.     

A software process for the construction of predictable on‐board embedded real‐time systems

The rise of the ‘cheaper, faster, better’ mission paradigm increasingly challenges the industrial development of satellite systems. The novel paradigm will have a profound impact on the production of the real‐time software embedded on board new‐generation systems. This paper contends that a large proportion of the ensuing demands can be satisfied by an iterative and incremental development model revolving around two evolutionary enhancements to the present engineering approach, namely (1) static real‐time analysis as a key ingredient of the software verification process, and (2) an architectural paradigm centred on fixed priority preemptive scheduling. Copyright © 1999 John Wiley & Sons, Ltd.     

基于场景规约的构件式系统设计分析与验证

使用接口自动机及接口自动机网络来描述构件式系统的行为设计模型,使用UML顺序图表示基于场景的需求规约,对系统设计阶段的构件交互行为的动态兼容性进行形式化分析和检验.通过对接口自动机网络状态空间的分析,给出了一系列算法以检验系统行为的存在一致性以及几种不同形式的强制一致性性质,包括前向强制一致性、逆向强制一致性以及双向强制一致性等.     

Guidelines for supporting real‐time multi‐touch applications

Multi‐touch driven user interfaces are becoming increasingly prevalent because of their intuitiveness and because of the reduction in the associated hardware costs. In recognition of this trend, multi‐touch software frameworks (MSFs) have begun to emerge. These frameworks abstract the low level issues of multi‐touch software development and deployment. MSFs therefore enable software developers who are unfamiliar with the complexities of multi‐touch software development to implement and deploy multi‐touch applications more easily. However, some multi‐touch applications have real‐time system requirements, and at present, no MSFs provide support for the development and deployment of such real‐time multi‐touch applications. The implication of this is that software developers are unable to take advantage of MSFs and, therefore, are forced to handle the complexities of multi‐touch and real‐time systems development and deployment for themselves in an ad hoc manner. The primary consequence of this is that the multi‐touch and/or real‐time aspects of the application may not function correctly. In this paper, guidelines are presented for applying real‐time system concepts to support the development and deployment of real‐time multi‐touch applications using MSFs. This serves to increase the probability that the application will meet its timing requirements while also reducing the complexity of the development and deployment process associated with multi‐touch applications. Copyright © 2013 John Wiley & Sons, Ltd.     

Enhancing OSGi with real‐time Java support

OSGi was designed with embedded systems in mind, its current support is insufficient for coping with one main characteristic of many embedded systems: real‐time performance. This article analyzes different key issues in providing OSGi with real‐time Java performance covering motivational issues, and different integration ways and challenges stemming from the integration. It also contributes a general framework for introducing real‐time performance in OSGi, which is called the real‐time for OSGi framework. The framework uses real‐time Java virtual machines and the real‐time specification for Java. The adoption of this framework allows cyber‐physical systems to experience real‐time Java performance in their applications. The framework introduces several integration levels for OSGi and real‐time specification for Java, and specific real‐time OSGi services. An empirical implementation was carried out using standard software, which was extended with the new defined services. Copyright © 2012 John Wiley & Sons, Ltd.     

Composing and scheduling service‐oriented applications in time‐triggered distributed real‐time Java environments

During the last decade, the number of distributed application domains with temporal requirements has significantly augmented, arising the necessity of exploring new concepts and paradigms that allow, on the one hand, the development of dynamic and flexible distributed applications and, on the other hand, the reusability of code. Service‐oriented paradigms have been successfully applied to distributed environments, increasing their flexibility and allowing the reusability of their components. Besides, distributed real‐time Java technologies have shown to be a good candidate to deploy real‐time distributed applications. This paper presents a model for service‐oriented applications on a time‐triggered distributed real‐time Java environment, focusing on the definition of the temporal model of an application and its schedulability, applying and evaluating this model in real‐time service‐oriented composition algorithms. Copyright © 2012 John Wiley & Sons, Ltd.     

Simulation of resource synchronization in a dynamic real‐time distributed computing environment

Today, more and more distributed computer applications are being modeled and constructed using real‐time principles and concepts. In 1989, the Object Management Group (OMG) formed a Real‐Time Special Interest Group (RT SIG) with the goal of extending the Common Object Request Broker Architecture (CORBA) standard to include real‐time specifications. This group's most recent efforts have focused on the requirements of dynamic distributed real‐time systems. One open problem in this area is resource access synchronization for tasks employing dynamic priority scheduling. This paper presents two resource synchronization protocols that the authors have developed which meet the requirements of dynamic distributed real‐time systems as specified by Dynamic Scheduling Real‐Time CORBA (DSRT CORBA). The proposed protocols can be applied to both Earliest Deadline First (EDF) and Least Laxity First (LLF) dynamic scheduling algorithms, allow distributed nested critical sections, and avoid unnecessary runtime overhead. In order to evaluate the performance of the proposed protocols, we analyzed each protocol's schedulability. Since the schedulability of the system is affected by numerous system configuration parameters, we have designed simulation experiments to isolate and illustrate the impact of each individual system parameter. Simulation experiments show the proposed protocols have better performance than one would realize by applying a schema that utilizes dynamic priority ceiling update. Copyright © 2004 John Wiley & Sons, Ltd.     

Using Forward Reachability Analysis for Verification of Lossy Channel Systems

We consider symbolic on-the-fly verification methods for systems of finite-state machines that communicate by exchanging messages via unbounded and lossy FIFO queues. We propose a novel representation formalism, called simple regular expressions (SREs), for representing sets of states of protocols with lossy FIFO channels. We show that the class of languages representable by SREs is exactly the class of downward closed languages that arise in the analysis of such protocols. We give methods for computing (i) inclusion between SREs, (ii) an SRE representing the set of states reachable by executing a single transition in a system, and (iii) an SRE representing the set of states reachable by an arbitrary number of executions of a control loop. All these operations are rather simple and can be carried out in polynomial time.With these techniques, one can straightforwardly construct an algorithm which explores the set of reachable states of a protocol, in order to check various safety properties. We also show how one can perform model-checking of LTL properties, using a standard automata-theoretic construction. It should be noted that all these methods are by necessity incomplete, even for the class of protocols with lossy channels.To illustrate the applicability of our methods, we have developed a tool prototype and used the tool for automatic verification of (a parameterized version of) the Bounded Retransmission Protocol.     

移动支付协议PCMS的形式化分析和验证

移动电子商务协议的形式化分析和验证是近年来移动电子商务协议的一个重要研究热点。以一个支付网关为中心的匿名的移动电子商务支付协议PCMS为研究对象,建立了PCMS协议的时间自动机模型,并用计算树逻辑CTL公式描述PCMS协议的部分性质,最后利用模型检测工具UPPAAL对PCMS协议的无死锁、时效性、有效性和钱原子性进行检测验证。验证结果表明,以支付网关为中心的匿名的安全支付协议PCMS满足无死锁、时效性、有效性和钱原子性。     

IPv6邻居发现协议的形式化验证

采用模型检查技术,对IPv6的邻居发现协议的属性进行了形式化验证.该协议的模型由目前广泛用于设计和描述通信协议的MSC(message sequence charts)来描述,并通过线性时序逻辑说明该协议的属性.还提出了由MSC模型的线性化自动抽取协议属性的方法.     

Verifying Automata Specification of Distributed Probabilistic Real-Time Systems

In this paper,a qualitative model checking algorithm for verification of distributed probabilistic real-time systems(DPRS)is presented.The model of DPRS,called real-time proba bilistic process model(RPPM),is over continuous time domain.The properties of DPRS are described by using deterministic timed automata(DTA).The key part in the algorithm is to map continuous time to finite time intervals with flag variables.Compared with the existing algorithms,this algorithm uses more general delay time equivalence classes instead of the unit delay time equivalence classes restricted by event sequence,and avoids generating the equivalence classes of states only due to the passage of time.The result shows that this algorithm is cheaper.