嵌入式实时系统的软件需求检测

以需求描述模型HRFSM(hierarchical finite state machines based on rules)为基础,提出了一个嵌入式实时系统软件的动态执行模型(dynamic execution model,简称DEM)和基于该模型的检测方法.由于DEM能将控制流、数据流和时间有效地集成为一体,故提出的检测方法能检测嵌入式实时系统的软件需求的一致性和完全性.该检测方法由3种侧重点不同的检测形式组成,并能在检测过程中提供一些重要的检测信息.分析员可以利用基于该检测方法的工具灵活地对嵌入式实时系统的软件需求进行检测,以提高分析和检测软件需求的效率.     

嵌入式实时软件通用框架模型研究

框架是一种在某个领域获得软件重用的重要途径,描绘的是一个待建应用系统软件的主要结构.从实时嵌入式系统的两大特性着手,提出了一个通用的嵌入式实时软件框架模型,深入分析了该框架下的资源模型、时间模型、任务模型、调度模型和通信模型以及它们之间的相互依赖关系,并且进行了建模.该模型在某航空机载系统研究中得到了应用并切实提高了软件的开发效率和可维护性,具有一定的工程理论和应用价值.     

ASADAL/SIM: an incremental multi-level simulation and analysis tool for real-time software specifications

Despite considerable advancement in software engineering methods during the past three decades, requirements engineering of large and complex software systems still remains a difficult and active research problem. One such difficulty lies in developing correct and useful methods for the validation and verification of real-time software specifications. One way of analyzing and validating/verifying software specifications is to mathematically derive or prove desired system properties based on formal specification languages. A full scale system analysis using such formal methods is limited in practice because of the required mathematical skills and computational costs. Formal methods are often used to check only a few very critical real-time properties. Simulation is a complementary approach to testing various system characteristics and validating user requirements. It is especially good for providing a rough picture of final system behavior. This paper presents ASADAL/SIM, a tool for multi-level simulation and analysis of real-time software specifications. It is a subsystem of a larger computer-aided real-time software development environment called ASADAL, and complements ASADAL/PROVER, another subsystem of ASADAL which is a formal verification module.^1. With ASADAL/SIM, simulation primitives can be added to evolving specifications in order to assign stochastic behaviors to external entities and internal processes, and to build a simulation model. ASADAL/SIM can execute the model and, at the same time, demonstrate the final system behavior by graphically showing internal workings of the system; catch undesirable system behaviors with breakpoints; and present various analytical results and system statistics ASADAL/SIM, following ASADAL's philosophies of hierarchical system modeling and early system validation, allows users to simulate ‘evolving’ specifications at different, mixed, and wide levels of detail. In particular, algorithmic details may be specified for low level behavioral blocks, and simulated with abstract entities yet to be refined to such a level. This facilitates the tracking of critical data values at the specification level, and eases the next transformation into code level implementation. With ASADAL/SIM, ASADAL becomes an effective and comprehensive supporting tool for various existing software engineering approaches, particularly top-down refinement and incremental development practices. © 1998 John Wiley & Sons, Ltd.     

面向嵌入式实时软件的需求规约语言及检测方法

针对嵌入式实时软件需求规约及其检测问题,提出了基于层次并发有穷状态机的可合成的图形化建模语言RTRSM*(real-time requirements specification model*),利用转换有效期和事件预定机制来描述时间限制,能够较好地支持系统交互性和实时性的建模.为弥补RTRSM*作为操作性规约语言不便于性质描述的问题,提出了命题时序逻辑RITL(real-time interval temporal logic).该语言以时间状态序列为语义模型,具有基于区间和时间点的量化时间属性描述功能,能自然、全面地描述RTRSM*模型性质.介绍并讨论了基于两种语言的规约检测方法和技术,主要包括系统状态空间有穷的RTRSM*模型状态可达图的相关问题和规约的模拟执行.     

面向集控嵌入式实时软件的单元测试方法研究

针对集控嵌入式实时软件的组成和特点,搭建了适合该软件的仿真单元测试平台,并详细介绍了基于Testbed对该软件进行单元测试的过程。依据静态分析输出的质量度量模型值定量地评价了软件内在源码的质量,并基于圈复杂度度量值提出了一种优先级的动态分析测试策略,用监控到的控制流信息来分析程序的覆盖率,从而确保单元测试的充分性和有效性,提高测试效率,保证软件的质量。     

基于组件的嵌入式软件开发方法

根据嵌入式软件的特点,提出一种以模型为中心、基于组件的嵌入式软件开发方法。它以动态数据流图为系统模型对嵌入式软件的功能和性能需求进行了描述,由此提供了强大的描述和分析能力;通过基于特定组件模型的实现结构和实现代码框架的自动生成,以DDF定义的系统可以被有效地分解为一系列独立的组件,合适的DDF调度算法一致地表示了系统组件的执行语义,使得并发开发的组件具有良好的可集成性。该方法充分考虑了嵌入式开发的特点,能有效地降低系统复杂性和支持系统组件的并发开发和复用,从而提高了开发效率并降低了开发成本。     

基于构件的嵌入式实时软件组合时间分析研究

在嵌入式实时软件的开发早期,将构件技术应用于对其进行时间需求的形式化分析中,不但有助于保证软件的正确性和可靠性,还能缩短需求分析周期、提高软件生产率。给出了一种基于构件技术、UML和时间ER网技术的组合时间分析方法,对嵌入式实时软件的时间需求进行分析和检测,实践表明该方法可以检测出需求模型中的时间冲突,有助于保证嵌入式实时软件时间约束的正确性,而且其分析结果具有可复用、可扩展的优点。     

基于需求的航空嵌入式软件测试技术研究

针对航空机载软件的特点，提出了一种基于需求的航空嵌入式软件测试模型，并对该模型中主要部分的功能及其相互关系进行了阐述，最后，最介绍了该模型在实际工程项目中的应用情况。     

实时嵌入式构件模型组装方法及时间性推理

针对实时嵌入式系统特点,提出一种可行的具有较好普适性的软构件模型及构件组装机制,使用形式化方法描述构件接口规约及组装规约,并给出构件时间性的推理方法,旨在实时嵌入式系统中构建更加通用、简易、开放的构件模型和更加合理的构件组装推理机制。     

基于构图覆盖的软件需求检测方法

以需求描述模型RTRSM为基础，通过建立抽象的、能将控制流和数据流等有机地结合到一起的实时软件的动态执行模型，提出了构图覆盖的动态检测方法，并给出了其具体算法．该方法能检测嵌入式实时软件系统动态执行步中各并行成分及其相互间的执行情况，而且也可为分析员提供一些有用的检测信息以提高分析和检测软件需求的效率．     

Communications-oriented development of component-based vehicular distributed real-time embedded systems

We propose a novel model- and component-based technique to support communications-oriented development of software for vehicular distributed real-time embedded systems. The proposed technique supports modeling of legacy nodes and communication protocols by encapsulating and abstracting the internal implementation details and protocols. It also allows modeling and performing timing analysis of the applications that contain network traffic originating from outside of the system such as vehicle-to-vehicle, vehicle-to-infrastructure, and cloud-based applications. Furthermore, we present a method to extract end-to-end timing models to support end-to-end timing analysis. We also discuss and solve the issues involved during the extraction of these models. As a proof of concept, we implement our technique in the Rubus Component Model which is used for the development of software for vehicular embedded systems by several international companies. We also conduct an application-case study to validate our approach.     

基于图元的嵌入式组态软件的设计与实现

为解决传统的自动控制软件设计中出现的开发周期长,代码复用率低等缺点,图形化的组态软件应运而生,它是模块的任意组合,用户可以根据自己的控制对象和控制目的任意组态.介绍了基于Linux的嵌入式图形组态软件的体系结构,阐述了基于图元的组态软件的设计思想、方法,强调了图元库的管理,以及根据图元属性再生图形和具体实现,最后给出了该软件平台的一个应用实例.     

航空机载嵌入式控制软件需求建模的形式化工程方法

嵌入式控制软件是现代航空飞行器的核心部件之一。构建软件需求的形式化规约精确地刻画人们对软件期望的功能和运行场景,是确保此类安全攸关软件质量的根本途径。在工业界,形式化需求建模的大规模应用尽管有成功的案例,但仍面临众多的困难。其根本性难点在于缺少一种系统化的工程方法来引导工业界软件实践者,从原始需求开始最终完成形式化需求规约,并能确认该规约真实、充分地反映了人们对软件期望的功能。针对上述挑战,提出了一种面向机载控制软件需求建模的形式化工程方法ACSDL-MV,以形式化方法为理论基础,结合软件需求工程的基本原理,引导工程人员从原始需求出发以演化式的过程逐步完成需求规约的构建;定制了航空控制软件的形式化描述语言ACSDL,用以构建形式化规约;为了确认软件需求规约准确、充分地描述了人们对软件期望的功能,该方法给出了基于图形的静态审查和基于模型的动态模拟技术。在航空发动机公司中的实验结果表明,该方法相比传统方法探测到了更多的潜在错误。     

常用嵌入式实时操作系统比较分析

以与实时系统开发过程密切相关的实时性、故障容错和标准兼容性等关键特征为基础,提出一套对嵌入式实时操作系统性能衡量的标准,涵盖体系结构、硬件支持、调度管理、内存管理、进程间通讯、定时性能、网络支持、文件系统、驱动编程以及开发调试等关键特证。并利用该标准对常用嵌入式实时操作系统进行了详细地分析与对比,为系统研发过程中嵌入式实时操作系统的选择提供指南。     

嵌入式软件测试工程化研究与实践

随着嵌入式系统在各行各业应用的迅速发展,其核心控制软件也变得日益庞大和复杂,实行有效的嵌入式软件测试显得越来越重要.首先分析了嵌入式软件的特点及嵌入式软件测试的重要性,接着阐述了一种有效的嵌入式软件测试工程化方法,并结合一个实际测试项目验证了该方法的有效性.     

嵌入式系统底层驱动可视化配置映射规则挖掘

汽车电子嵌入式控制软件底层驱动的可视化配置屏蔽了底层实现细节,降低了配置难度,方便用户应用。但是,可视化配置的结构体嵌套使映射出的软件界面元素规则复杂化,且扩展芯片各模块结构体的未知性,使得映射规则难以普遍适用。为此,提出了一种可视化配置映射规则的挖掘方法,开发了针对芯片各模块结构体进行初始化配置的软件。通过对不同芯片底层驱动的实际配置,证实了该方法的有效性。     

开放式实时嵌入式系统自适应调度模型研究

开放式实时嵌入式系统中多类型实时任务并存和资源受限的情况给实时调度机制带来了新的需求和挑战。通过引入准入控制、资源管理、调度服务器、自适应调节机制等,提出了一个形式化的自适应调度模型。它能适应开放计算环境的不确定性,有控制地接受不同类型任务的运行;可根据系统资源和任务需求的最新变换情况计算带宽变化,自适应地调节任务的优先等级,使得系统运行在最优的实时性能上;该模型在某航空机载系统设计中得到了实际应用,同其它类似系统相比,该模型的应用提高了系统的调度性和系统稳定性。     

嵌入式组态软件脚本解释虚拟机的设计

为了增强嵌入式组态软件的功能,引入一种类似于C语言的脚本.设计一个编译器把该脚本编译成中间代码,采用中间代码的优点是可提高程序运行的速度,也减小了脚本解释程序的设计难度.提出一种仿微处理器结构的脚本虚拟机设计方案,在运行时对中间代码进行解释.虚拟机主要由程序存储器、指令译码器、运算器、程序计数器、控制器以及动态容器组成,其中动态容器的设计是关键,它具有可动态分配内存、自动释放内存等优点,适合于嵌入式操作系统下运行.实验与测试结果表明,该脚本解释虚拟机可满足嵌入式组态软件设计的要求.     

嵌入式实时Web Server的动态调度算法研究

对嵌入式实时Web Server的网络任务活动特点进行了研究,将任务分为优先任务和普通任务两类,在此基础上利用M／M／1/K模型提出了保障优先任务接纳率的动态调度算法。该方法可以根据实时Web Server当前的任务量决定是否接纳普通任务,保证实时Web Server在优先任务安全运行的前提下,为网络中的其它客户开放资源。该算法已用于远程实验网站的任务调度(www．remot-lab．net)。     

Automated structural analysis of SCR‐style software requirements specifications using PVS

The importance of effective requirements analysis techniques cannot be overemphasized when developing software requiring high levels of assurance. Requirements analysis can be largely classified as either structural or functional. The former investigates whether definitions and uses of variables and functions are consistent, while the latter addresses whether requirements accurately reflect users' needs. Verification of structural properties for large and complex software requirements is often repetitive, especially if requirements are subject to frequent changes. While inspection has been successfully applied to many industrial applications, the authors found inspection to be ineffective when reviewing requirements to find errors violating structural properties. Moreover, current tools used in requirements engineering provide only limited support in automatically enforcing structural correctness of the requirements. Such experience has motivated research to automate straightforward but tedious activities. This paper demonstrates that a theorem prover, PVS (Prototype Verification System), is useful in automatically verifying structural correctness of software requirements specifications written in SCR (Software Cost Reduction)‐style. Requirements are automatically translated into a semantically equivalent PVS specification. Users need not be experts in formal methods or power users of PVS. Structural properties to be proved are expressed in PVS theorems, and the PVS proof commands are used to carry out the proof automatically. Since these properties are application independent, the same verification procedure can be applied to requirements of various software systems. Copyright © 2001 John Wiley & Sons, Ltd.