一种SysML模型到AADL模型的自动转换方法

安全关键系统的实现需要通过需求、设计、集成、验证和测试等多个阶段。近年来,模型驱动开发方法逐渐成为安全关键系统设计与开发的重要手段。由于还没有一个建模语言能够支持整个安全关键系统开发生命周期,因此选择集成使用2种广泛使用的标准语言:系统建模语言(SysML)和嵌入式实时系统体系结构分析与设计语言(AADL)。SysML和AADL提供了同一系统的2个不同视图,SysML模型为系统工程师提供了一个系统视图,AADL为架构设计师建立一个较低层次的设计视图,它结合了实现所有功能的硬件、操作系统和代码。提出一种SysML模型到AADL模型的自动转换方法。首先,定义SysML子集SubSysML,主要包括模块定义图(BDD)、内部模块图(IBD)、活动图(ACT)子集和从IBD和BDD扩展的AADL Profile;其次,定义SubSysML到AADL的转换规则并设计转换算法;然后,对生成的AADL初始模型进行精化;最后,使用EMF框架技术实现SubSysML到AADL的模型转换工具并通过雷达案例验证所提方法的有效性。     

<Emphasis Type="Italic">SetExp</Emphasis>: a method of transformation of timed automata into finite state automata

Real-time discrete event systems are discrete event systems with timing constraints, and can be modeled by timed automata. The latter are convenient for modeling real-time discrete event systems. However, due to their infinite state space, timed automata are not suitable for studying real-time discrete event systems. On the other hand, finite state automata, as the name suggests, are convenient for modeling and studying non-real time discrete event systems. To take into account the advantages of finite state automata, an approach for studying real-time discrete event systems is to transform, by abstraction, the timed automata modeling them into finite state automata which describe the same behaviors. Then, studies are performed on the finite state automata model by adapting methods designed for non real-time discrete event systems. In this paper, we present a method for transforming timed automata into special finite state automata called Set-Exp automata. The method, called SetExp, models the passing of time as real events in two types: Set events which correspond to resets with programming of clocks, and Exp events which correspond to the expiration of clocks. These events allow to express the timing constraints as events order constraints. SetExp limits the state space explosion problem in comparison to other transformation methods of timed automata, notably when the magnitude of the constants used to express the timing constraints are high. Moreover, SetExp is suitable, for example, in supervisory control and conformance testing of real-time discrete event systems.     

On condition/event systems with discrete state realizations

This paper introduces condition/event (C/E) systems as a class of continuous-time discrete event dynamic systems (DEDS) with two types of discrete-valued input and output signals:condition signals andevent signals. In applications such as discrete control, C/E systems provide an intuitive continuous-time modeling framework amenable to block diagram representation. In this paper we consider C/E systems with discrete state realizations, and study the relationship between continuous-time C/E systems and untimed models of their sequential inputoutput behavior called C/E languages. We show that C/E systems with discrete state realizations are necessarilytime-change invariant (Theorem 3.1), which means the ensemble of admissible continuous-time input-output behaviors is completely characterized by the C/E language for the system (Theorem 4.1). It is also shown that deterministic C/E systems with discrete state realizations are necessarily discrete-time (clocked) systems (Corollary 3.1), and that finite discrete state realizations exist for a C/E system only if its related C/E language has a finite state generator (Theorem 4.2). Finally, we develop equivalent discrete-state realizations for C/E systems resulting from cascade and feedback interconnections. The paper concludes with a discussion of several directions for future research.Please direct correspondence concerning this paper to B.H. Krogh at the above address.     

A formal mathematical framework for modeling probabilistic hybrid systems

The development of autonomous agents, such as mobile robots and software agents, has generated considerable research in recent years. Robotic systems, which are usually built from a mixture of continuous (analog) and discrete (digital) components, are often referred to as hybrid dynamical systems. Traditional approaches to real-time hybrid systems usually define behaviors purely in terms of determinism or sometimes non-determinism. However, this is insufficient as real-time dynamical systems very often exhibit uncertain behavior. To address this issue, we develop a semantic model, Probabilistic Constraint Nets (PCN), for probabilistic hybrid systems. PCN captures the most general structure of dynamic systems, allowing systems with discrete and continuous time/variables, synchronous as well as asynchronous event structures and uncertain dynamics to be modeled in a unitary framework. Based on a formal mathematical paradigm exploiting abstract algebra, topology and measure theory, PCN provides a rigorous formal programming semantics for the design of hybrid real-time embedded systems exhibiting uncertainty.      

Constructivist foundations of modeling—A Kantian perspective

By linking Knowledge Engineering to Kantian Philosophy, this paper attempts to elaborate a potential theoretical foundation for understanding the nature of expertise and the processes of modeling. The established way of modeling is criticized for presuming the relation between the real objective world and the AI software models being a “mapping” (abstraction, copy, representation, etc.) relation. The paper argues that this aspect of the foundations of modeling in Knowledge Engineering could be improved by employing the standpoint presented in Kant's Critique of Pure Reason. Two hypotheses and ten principles of a constructivist modeling paradigm based on Kant's work are proposed. The term Constructivist here refers to the hypothesis that a model cannot “correspond to” reality but merely be “viable in” (i.e., “fit into”) reality. © John Wiley & Sons, Inc.     

Hybrid MARTE statecharts

The specification of modeling and analysis of real-time and embedded systems (MARTE) is an extension of the unified modeling language (UML) in the domain of real-time and embedded systems. Even though MARTE time model offers a support to describe both discrete and dense clocks, the biggest effort has been put so far on the specification and analysis of discrete MARTE models. To address hybrid real-time and embedded systems, we propose to extend statecharts using both MARTE and the theory of hybrid automata. We call this extension hybrid MARTE statecharts. It provides an improvement over the hybrid automata in that: the logical time variables and the chronometric time variables are unified. The formal syntax and semantics of hybrid MARTE statecharts are given based on labeled transition systems and live transition systems. As a case study, we model the behavior of a train control system with hybrid MARTE statecharts to demonstrate the benefit.     

Contract-based modeling and verification of timed safety requirements within SysML

In order to cope with the growing complexity of critical real-time embedded systems, systems engineering has adopted a component-based design technique driven by requirements. Yet, such an approach raises several issues since it does not explicitly prescribe how system requirements can be decomposed on components nor how components contribute to the satisfaction of requirements. The envisioned solution is to design, with respect to each requirement and for each involved component, an abstract specification, tractable at each design step, that models how the component is concerned by the satisfaction of the requirement and that can be further refined toward a correct implementation. In this paper, we consider such specifications in the form of contracts. A contract for a component consists in a pair (assumption, guarantee) where the assumption models an abstract behavior of the component’s environment and the guarantee models an abstract behavior of the component given that the environment behaves according to the assumption. Therefore, contracts are a valuable asset for the correct design of systems, but also for mapping and tracing requirements to components, for tracing the evolution of requirements during design and, most importantly, for compositional verification of requirements. The aim of this paper is to introduce contract-based reasoning for the design of critical real-time systems made of reactive components modeled with UML and/or SysML. We propose an extension of UML and SysML languages with a syntax and semantics for contracts and the refinement relations that they must satisfy. The semantics of components and contracts is formalized by a variant of timed input/output automata on top of which we build a formal contract-based theory. We prove that the contract-based theory is sound and can be applied for a relatively large class of SysML system models. Finally, we show on a case study extracted from the automated transfer vehicle (http://www.esa.int/ATV) that our contract-based theory allows to verify requirement satisfaction for previously intractable models.     

Towards a traceability model in a MARTE-based methodology for real-time embedded systems

This paper addresses the traceability management in the context of Accord_|UML, a MARTE-based methodology for designing distributed real-time embedded systems. Our contribution is two fold: on the one hand, we propose to include directly requirements in the modeling process; on the other hand, we identify potential traceability links that we model by using the SysML requirement profile. We also present the toolbox that supports our contribution. This work is partly funded by the French Research Agency (ANR) in the context of the “Réseau National des Technologies Logicielles” support within both MeMVaTEx and Domino Projects.     

A formal verification framework for SysML activity diagrams

SysML activity diagrams are OMG/INCOSE standard diagrams used for modeling and specifying probabilistic systems. They support systems composition by call behavior and send/receive artifacts. For verification, the existing approaches dedicated to these diagrams are limited to a restricted set of artifacts. In this paper, we propose a formal verification framework for these diagrams that supports the most important artifacts. It is based on mapping a composition of SysML activity diagrams to the input language of the probabilistic symbolic model checker called “PRISM”. To prove the soundness of our mapping approach, we capture the underlying semantics of both the SysML activity diagrams and their generated PRISM code. We found that the probabilistic equivalence relation between both semantics preserve the satisfaction of the system requirements. Finally, we demonstrate the effectiveness of our approach by presenting real case studies.     

Intra-Period (Within-Day) Dynamic Models for Continuous Services

To simulate important aspect of some transportation systems (e.g. demand peaks, temporary capacity variations, temporary over-saturation of supply elements, and formation and dispersion of queues) a new class of models, referred to in the literature as Dynamic Traffic Assignment (DTA) models, have been recently developed. Although Dynamic Traffic Assignment to networks is a relatively new research subject, a great number of models have been proposed in the last two decades. These can be divided in two main classes according to the typology of service they aim at simulating. These are continuous services, considering transportation services available at any time and accessible from several points, such as the services offered by individual road modes (car, bicycle etc.), and scheduled services simulating services available only at certain times and that can be accessed only at certain locations (terminals, stations, airports etc.). In this paper the focus is on continuous services. Models proposed in the literature are reviewed and classified according to basic assumptions on the flow structure, i.e. whether a continuous or a discrete approach is followed, and on the representation of time (discrete vs. continuous). A general modeling framework consisting of supply, demand, and demand-supply interaction models, and including most of the existing specifications is presented both for the discrete time-discrete flow and continuous time continuous flow cases.     

VERTAF/Multi-Core: A SysML-Based Application Framework for Multi-Core Embedded Software Development

Multi-core processors are becoming prevalent rapidly in personal computing and embedded systems.Nevertheless,the programming environment for multi-core processor-based systems is still quite immature and lacks efficient tools.In this work,we present a new VERTAF/Multi-Core framework and show how software code can be automatically generated from SysML models of multi-core embedded systems.We illustrate how model-driven design based on SysML can be seamlessly integrated with Intel’s threading building blocks (TBB) and the quantum framework (QF) middleware.We use a digital video recording system to illustrate the benefits of the framework.Our experiments show how SysML/QF/TBB help in making multi-core embedded system programming model-driven,easy,and efficient.     

An event-based approach for formally verifying runtime adaptive real-time systems

Real-time and embedded systems are required to adapt their behavior and structure to runtime unpredicted changes in order to maintain their feasibility and usefulness. These systems are generally more difficult to specify and verify owning to their execution complexity. Hence, ensuring the high-level design and the early verification of system adaptation at runtime is very crucial. However, existing runtime model-based approaches for adaptive real-time and embedded systems suffer from shortcoming linked to efficiently and correctly managing the adaptive system behavior, especially that a formal verification is not allowed by modeling languages such as UML and MARTE profile. Moreover, reasoning about the correctness and the precision of high-level models is a complex task without the appropriate tool support. In this work, we propose an MDE-based framework for the specification and the verification of runtime adaptive real-time and embedded systems. Our approach stands for Event-B method to formally verify resources behavior and real-time constraints. In fact, thanks to MDE M2T transformations, our proposal translates runtime models into Event-B specifications to ensure the correctness of runtime adaptive system properties, temporal constrains and nonfunctional properties using Rodin platform. A flood prediction system case study is adopted for the validation of our proposal.

     

基于UML-RT的复杂嵌入式系统建模方法及其应用

分析了UML在实时系统设计中的优点和需要解决的主要问题,论述了基于UML RT的实时嵌入式系统设计方法,并且对其进行扩展以支持数据流计算模型的建模,最后以汽车巡航系统为例加以说明。     

Discrete port-Hamiltonian systems

Either from a control theoretic viewpoint or from an analysis viewpoint it is necessary to convert smooth systems to discrete systems, which can then be implemented on computers for numerical simulations. Discrete models can be obtained either by discretizing a smooth model, or by directly modeling at the discrete level itself. One of the goals of this paper is to model port-Hamiltonian systems at the discrete level. We also show that the dynamics of the discrete models we obtain exactly correspond to the dynamics obtained via a usual discretization procedure. In this sense we offer an alternative to the usual procedure of modeling (at the smooth level) and discretization.     

CFSM: a novel frame analyzing mechanism for real-time face recognition system on the embedded system

The development of web cameras and smart phones is mature, and more and more facial recognition-related applications are implemented on embedded systems. The demand for real-time face recognition on embedded systems is also increasing. In order to improve the accuracy of face recognition, most of the modern face recognition systems consist of multiple deep neural network models for recognition. However, in an embedded system, integrating these complex neural network models and execute simultaneously is not easy to achieve the goal of real-time recognition of human faces and their identities. In view of this, this study proposes a new frame analysis mechanism, continuous frames skipping mechanism (CFSM), which can analyze the frame in real time to determine whether it is necessary to perform face recognition on the current frame. Through the analysis of CFSM, the frames that do not need to be re-recognized for face are omitted. In this way, the workload of the face recognition system will be greatly reduced to achieve the goal of real-time face recognition in the embedded system. The experimental results show that the proposed CFSM mechanism can greatly increase the speed of face recognition in the video on the embedded system, achieving the goal of real-time face recognition.

     

The score function approach for sensitivity analysis of computer simulation models

Some theoretical and practical aspect of the score function (SF) approach for estimating the sensitivities of computer simulation models and solving the so-called “what if” problem (performance extrapolation) are considered. It is shown that both the sensitivities (gradients, Hessians, etc.) and the performance extrapolation can be derived simultaneously by simulating only a single sample path from the nominal system. It is also shown that the SF approach can be efficiently applied for DESS (discrete event static systems, example: reliability models and stochastic networks) and for DEDS (discrete events dynamic systems, example: queuing networks) under light traffics. Control variates procedure for variance reduction is presented as well     

HOPE: a hybrid deep neural model for out-of-town next POI recommendation

Next Point-of-interest (POI) recommendation has been recognized as an important technique in location-based services, and existing methods aim to utilize sequential models to return meaningful recommendation results. But these models fail to fully consider the phenomenon of user interest drift, i.e. a user tends to have different preferences when she is in out-of-town areas, resulting in sub-optimal results accordingly. To achieve more accurate next POI recommendation for out-of-town users, an adaptive attentional deep neural model HOPE is proposed in this paper for modeling user’s out-of-town dynamic preferences precisely. Aside from hometown preferences of a user, it captures the long and short-term preferences of the user in out-of-town areas using “Asymmetric-SVD” and “TC-SeqRec” respectively. In addition, toward the data sparsity problem of out-of-town preference modeling, a region-based pattern discovery method is further adopted to capture all visitor’s crowd preferences of this area, enabling out-of-town preferences of cold start users to be captured reasonably. In addition, we adaptively fuse all above factors according to the contextual information by adaptive attention, which incorporates temporal gating to balance the importance of the long-term and short-term preferences in a reasonable and explainable way. At last, we evaluate the HOPE with baseline sequential models for POI recommendation on two real datasets, and the results demonstrate that our proposed solution outperforms the state-of-art models significantly.

     

基于数字孪生的产线设备实时监控方法与实现

为推动国家智能制造发展,面向生产过程中设备实时监控困难、透明性差、管控效率低、跨学科交叉情况复杂等问题,融合MBSE思想,提出一种基于数字孪生的产线设备监控方法并实现。首先,提出基于数字孪生的监控方法架构;基于SysML建模语言对产线系统和设备进行统一描述建模,建立结构图和行为图,形成数据模型;通过SysML模型与OPC UA联合,以位移数据和任务数据双通道驱动的方式进行虚实映射,并建立异常报警追溯机制;以仓储系统中核心设备堆垛机为例,构建其SysML模型、数字孪生模型,并以仓储产线实时缓存数据库redis为数据源,通过OPC UA获取并实时更新数据驱动数字孪生模型,实现其三维可视化监控,验证了方法的可行性和实时性     

CONCEPTS OF FUZZY INFORMATION MEASURES ON CONTINUOUS DOMAINS

Measures of information based on fuzzy sets (possibility distributions) had been defined only for finite domains of discourse. This paper presents a method of defining such information functions on a continuous universe of discourse—a domain which is a measurable space of measure 1. The method is based on the concept of “rearangement” of a function, used in lieu of sorting discrete possibility values. For technical reasons, it is preferred to express information value as information distance to the most “uninformed” (constant possibility 1) distribution. The final form of the information for possibility distribution f is

The paper then discusses related information distances and approximations using discrete information functions.     

A Model-based approach for the synthesis of software to firmware adapters for use with automatically generated components

This paper presents the MDE process in use at Elettronica SpA (ELT) for the development of complex embedded systems integrating software and firmware. The process is based on the adoption of SysML as the system-level modeling language and the use of Simulink for the refinement of selected subsystems. Implementations are generated automatically for both the software (C++ code) and firmware parts, and communication adapters are automatically generated from SysML using a dedicated profile and open-source tools for modeling and code generation. The process starts from a SysML system model, developed according to the platform-based design paradigm, in which a functional model of the system is paired to a model of the execution platform. Subsystems are refined as Simulink models or hand-coded in C++. An implementation for Simulink models is generated as software code or firmware on FPGA. Based on the SysML system architecture specification, our framework drives the generation of Simulink models with consistent interfaces, allows the automatic generation of the communication code among all subsystems (including the HW–FW interface code). In addition, it provides for the automatic generation of connectors for system-level simulation and of test harnesses and mockups to ease the integration and verification stage. We provide early results on the time savings obtained by using these technologies in the development process.