教学课程资源库 更多>>

关键词： Architecture description language   Model-driven development   Fractionated spacecraft  

摘要： Complex sensing, processing and control applications running on distributed platforms are difficult to design, develop, analyze, integrate, deploy and operate, especially if resource constraints, fault tolerance and security issues are to be addressed. While technology exists today for engineering distributed, real-time component-based applications, many problems remain unsolved by existing tools. Model-driven development techniques are powerful, but there are very few existing and complete tool chains that offer an end-to-end solution to developers, from design to deployment. There is a need for an integrated model-driven development environment that addresses all phases of application lifecycle including design, development, verification, analysis, integration, deployment, operation and maintenance, with supporting automation in every phase. Arguably, a centerpiece of such a model-driven environment is the modeling language. To that end, this paper presents a wide-spectrum architecture design language called DREMS ML that itself is an integrated collection of individual domain-specific sub-languages. We claim that the language promotes "correct-by-construction" software development and integration by supporting each individual phase of the application lifecycle. Using a case study, we demonstrate how the design of DREMS ML impacts the development of embedded systems. (C) 2015 Elsevier B.V. All rights reserved.

关键词： STPA   CTCS-3级列控系统   形式化方法   功能安全分析  

摘要： 本文给出CTCS-3级列控系统中组件控制行为的形式化定义,并针对控制行为的时序关系,提出控制行为时序逻辑。以此时序逻辑为基础,给出控制关系模型的形式化定义,使用控制关系模型对列控系统中的控制行为关系进行刻画。利用深度优先搜索的方式,对系统的控制关系模型进行分析,实现STPA(System-Theoretic Process Analysis)过程中不恰当控制行为的自动化辨识。以CTCS-3级列控系统的RBC交接场景为例,使用上述基于控制关系模型的STPA方法对列控系统的功能安全进行分析。分析过程表明利用形式化的控制关系模型扩展STPA的方法适用于CTCS-3级列控系统的功能安全分析。

关键词： Biofuels reforming   Structured catalysts   Microchannel and foam substrates   Ru-Ni alloy nanoparticles   Perovskite-like and fluorite-like oxide supports   Catalytic performance  

摘要： Catalysts for biofuels reforming based on two types of nanocomposite active components( Ni + Ru/La0.8Pr0.2Mn0.2Cr0.8O3/Y0.08Zr0.92O2-delta, Ni + Ru/Sm0.15Pr0.15Ce0.35Zr0.35O2) supported on microchannel substrates (Ni-Al alloy foam plates, Fechraloy plates protected by a thin corundumlayer) were developed. Applied procedures for the active components loading on substrates provide thermochemical stability of supported layers of active components in tough operation conditions not affecting their reactivity/catalytic activity. Effects of the nature of nanocomposite active component, type of fuel (ethanol, ethyl acetate, acetone and glycerol), feed composition and contact time on the yield of syngas/byproducts and performance stability are considered and compared with results of calculations of the equilibrium composition of reaction mixtures. For nanocomposite active components with a high oxygen mobility and reactivity, reforming of such typical fuel as ethanol is described by the stepwise red-ox mechanism. Preliminary results of the mathematical modelling of the ethanol steam reforming on a stack of microchannel Fechraloy plates loaded with Ni + Ru/Sm 0.15Pr0.15Ce0.35Zr0.35O2 active component revealed that this process can be satisfactorily described by the isothermal model without any impact of the heat/mass transfer. (C) 2014 Elsevier B.V. All rights reserved.

关键词： 事件本体   事件要素投影   形式化   扩展描述逻辑  

摘要： 文本事件的表示一直缺乏针对事件要素的有效表示和推理方法,采用传统描述逻辑对基于事件的知识进行形式化表示存在表达能力不足的问题.提出一种新的事件本体结构模型,在此基础上对描述逻辑的子语言SROIQ进行扩展,同时提出事件要素投影理论实现对事件本体的形式化.该方法利用SROIQ丰富的表达能力,将动态的事件转换为静态的复杂概念,既统一了事件与事件状态的表示方法,也建立起了事件之间、事件要素之间的语义关系.基于SROIQ的事件要素投影方法能够有效表示各领域的事件类、事件实例与事件要素,提取事件、事件关系在事件要素上的普遍规律,有助于领域事件本体的构建和形式化,以及针对事件要素的推理.

关键词： 结构化设计   道路桥梁设计   应用  

摘要： 伴随着社会经济的高度发展,显著推动了交通运输业的发展进程,而道路桥梁设计在交通运输业中占据着重要的位置。本文先简单分析在道路桥梁设计中应用结构化设计的重要性,然后对结构化设计进行概述,最后探讨结构化设计的具体应用,希望能为道路桥梁设计提供一定的参考。

关键词： Model driven development   Round-trip engineering   3D applications   Virtual reality   Augmented reality   Model transformation   Model differences   Model merging  

摘要： While structured software development processes are nowadays common-place, 3D applications are often still developed in an ad-hoc and code-centric manner. This state of affairs is somewhat surprising, as there are many benefits to a more structured 3D development process. In particular, model-based techniques with support for iterative development could help to ensure the mutual consistency of the code bases produced by the heterogeneous developer groups, i.e. 3D content developers and programmers. However, a cultural gap exists between 3D content developers and programmers who use completely different tools and terminologies. Common tools for model-driven development, for instance based on UML, are inadequate for the often "creatively oriented" 3D content developers. This paper presents a model-driven approach for the structured development of 3D applications in interdisciplinary teams based on round-trip engineering. Abstract models of the application are specified in SSIML, a DSL tailored for the development of 3D applications. In a forward phase, consistent skeletons of 3D scene models and program code are generated from the SSIML model. In a reverse phase, refinements of both the 3D scene model and program code are abstracted and synchronized to result in an updated SSIML model. This process is repeated in the subsequent iterations. Several examples of 3D application development on diverse platforms including Web, immersive virtual reality, and augmented reality on mobile devices demonstrate the versatility of our approach.

关键词： FPGA   Detailed routing   Boolean satisfiability   Switch box architecture  

摘要： Detailed routing solutions for island style FPGA architectures using Boolean satisfiability (SAT) based formulations have been proposed in this paper. Due to decreasing size of ICs and hence, the increasing complexity of the routing resource constraints, routing has been a big challenge in electronic design automation field. Our proposed techniques work on multi-pin net routing where all nets are considered for routing in their intact form whereas, most of the existing routing solutions decompose multi-pin nets into two-pin nets for detailed routing to ease the problem. However this approach, apart from increasing the number of nets in the circuits, may also introduce pin doglegging which, when not permitted by the architecture of FPGA, would require extra constraints to eliminate. Many detailed routers adopt sequential detailed routing approaches which are vulnerable to the net ordering problem which may cause a routable circuit to be erroneously classified as unroutable. Our proposed techniques avoid these pitfalls by keeping the multi-pin nets intact and solve all nets simultaneously using SAT. The SAT-based multi-pin net dogleg-free formulations presented here achieve significant improvement over existing SAT-based solutions with respect to the number of variables and clauses used, thereby achieving greater scalability and also display comparable and sometimes better mutability results on benchmark circuits when compared with other detailed routing solutions. Detailed routing is also significantly affected by the architecture of the switching blocks. This paper proposes SAT-based formulation for three different switch box architectures i.e. Subset, Wilton, and Universal switches. Our experiments clearly demonstrate how routing solutions for a circuit can differ significantly for different types of switch boxes. (C) 2015 Elsevier Ltd. All rights reserved.

关键词： AADL dependablity model   formal method   IMC model transformation   可靠性模型   形式化方法   AADL   IMC 模型转换   Language of Keywords: English   Chinese  

摘要： As embedded software Is widely used in safety-critical areas, its scale, complexity and performance demand increase, so system reliablity becomes increasingly important. Architecture analysis and design language (AADL) is an important way for architecture modeling, analysss, and verification in the field of embedded systems and it has gradually become the industry standard. Because AADL is not a full formal model, accurate description of its semantics is required to do quantitative analysss. In this paper we propose an AADL-based software system reliability modeling and evaluation framework. We generate an AADL dependabllity model based on the AADL model and the AADL error model. The basic elements and the spedal elements (e. g. error propagation) of the AADL dependabllity model are transformed into the interactive Markov chains (IMC) model by applying model transformation rules and the resulting IMC quantitative analysss is conducted. The modeling approach is applied to a subsystem of the French Air Traffic Control System, and its feasibllity and effectiveness are proved. [ABSTRACT FROM AUTHOR]

关键词： 软件工程   课程改革   CMM   案例教学  

摘要： 基于CMM核心理念,设计三个由简单到复杂的软件小项目,在软件工程实践教学中应用,分析应用过程中所收集到的数据。分析表明,逐步引入CMM核心理念的实践教学方法可以协助学生更好的理解和掌握软件工程的基本概念与基本原理,可以提升学生掌握相关的基本技能的效率,可以提升学生的软件组织开发能力。

关键词： Polarimetry   Polarization   Scattering  

摘要： Partial Mueller matrix polarimeters (pMMPs) are active sensing instruments that probe a scattering process with a set of polarization states and analyze the scattered light with a second set of polarization states. Unlike conventional Mueller matrix polarimeters, pMMPs do not attempt to reconstruct the entire Mueller matrix. With proper choice of generator and analyzer states, a subset of the Mueller matrix space can be reconstructed with fewer measurements than that of the full Mueller matrix polarimeter. In this paper we consider the structure of the Mueller matrix and our ability to probe it using a reduced number of measurements. We develop analysis tools that allow us to relate the particular choice of generator and analyzer polarization states to the portion of Mueller matrix space that the instrument measures, as well as develop an optimization method that is based on balancing the signal-to-noise ratio of the resulting instrument with the ability of that instrument to accurately measure a particular set of desired polarization components with as few measurements as possible. In the process, we identify 10 classes of pMMP systems, for which the space coverage is immediately known. We demonstrate the theory with a numerical example that designs partial polarimeters for the task of monitoring the damage state of a material as presented earlier by Hoover and Tyo [Appl. Opt. 46, 8364 (2007)]. We show that we can reduce the polarimeter to making eight measurements while still covering the Mueller matrix subspace spanned by the objects. (C) 2015 Optical Society of America