基于AOP技术的软件性质监控框架

针对软件运行时可信保障存在的相关问题,提出了基于AOP技术的软件性质监控框架。本框架使用OCL(Object Constraint Language)和UML Profile的SPT(Schedulability,Performance and Time)规范实现了软件性质在模型上的描述,基于描述并独立于被监控软件自动生成监控方面,将监控方面编织入被监控软件,从而使被监控软件具有运行时软件性质监控能力。     

一种面向方面的软件组件监控模型

针对传统软件监控方法中模块化不好、缺乏灵活性的缺点,文中的模型中,将组件技术中的概念和方法应用于面向方面的技术中,提出了一个模块化、灵活性好的软件监控模型。在模型中将监控功能封装为一个面向方面的组件,有效解决了传统监控方法中因在应用代码中插入监控功能代码所产生的代码混乱与分散问题,也避免了因在组件和方面两个维度上考虑监控问题所产生的代码混乱与分散问题。     

监控使能的分布式软件系统构造方法

针对开放的网络环境中大型分布式软件的调试、调优、维护和可信演化问题,提出了伴随式的监控使能分布式软件构造方法.基于发布/订阅的分布计算模型,提出了被监控对象的业务逻辑和监控逻辑分离的运行时体系结构;基于面向方面编程思想,提出了监控使能的分布式软件开发方法和工具,降低了监控实施代价,增强了代码的可维护性;基于运行时体系结构,提出了监控系统的动态可定制部署方法.监控使能的分布式软件构造方法能够在开发时控制功能代码和非功能代码的纠结,尽可能地降低软件编程人员的代码维护难度;能够在部署时保证监控系统和被监控对象的松耦合;能够在运行时实现监控信息的按需汇聚和按需处理.从而在对系统核心业务的影响尽可能小的前提下.获得对系统运行行为尽可能全面的理解.     

基于嵌入式可信平台的运行时监控方法

当前可信计算平台缺乏对自身运行时安全属性的监控,对此,提出一种针对嵌入式可信平台的运行时监控方法。通过自动化的代码插入和运行时实时监控,保证可信平台的运行时安全功能符合设计规范,并保证系统性能和运行状态符合特定条件约束,同时对相应的异常进行实时处理。实验结果表明,随着监控节点数的增长,监控的准确性和实时性提高,而监控开销和异常处理开销处于合理范围。     

基于OCL的面向方面监控框架

基于面向方面编程技术提出一种软件性质监控框架。该框架根据对象约束语言的约束条件生成监控方面,对监控方面与被监控软件进行编织,使软件在运行时具备发现约束违背的能力。使用模型约束检查工具USE可以进一步分析违约信息,实现其在模型上的可视化呈现。     

自适应重配置软件系统的运行时监控方法研究

运行时监控技术作为实现自适应软件的一个重要研究内容,现已成为当前很多软件工程方法中用来提高软件产品可信性的一个重要设计原则。针对现有的很多软件监控方法常常将系统的监控逻辑与业务功能逻辑混杂在一起的问题,提出了一个需求模型驱动的、自适应重配置软件的运行时监控方法。以软件系统的目标模型及属性规约为基础,介绍了如何构建系统的监控模型、生成和编织监控代码,以及进行运行时诊断分析和自适应重配置调整。该方法通过采用独立于应用程序的外部单元来实现对运行时系统的监控、诊断和自适应重配置处理。这更利于系统的维护和管理,也更符合软件复用的思想。     

植入式安全性质监控技术

针对安全性质,提出一种植入式监控方法.使用OCL(Object Constraint Language)实现安全性质在模型上的描述,并将OCL约束转化为Java监控代码,从而实现监控信息由模型到代码的映射.该方法采用AOP(Aspect-Oriented Programming)技术将监控代码植入目标系统,使软件在运行时具备安全性质的监控能力.     

基于PAR的算法形式化开发

形式化方法是构建可信软件的重要途径.基于对算法问题的分析,针对形式化方法PAR开发算法的特征,刻划了问题分划、递推关系构造方面的规律.从一类问题的形式化功能规约出发,可机械地完成问题的分划及规约的变换,自然地揭示出求解问题的算法思想,在相关工具的支持下自动生成算法程序.研究结果将算法设计中尽可能多的创造性劳动转化为非创造性劳动,降低了形式化求解算法问题的难度,提高了算法程序的可靠性和形式化开发效率.     

支持运行监控的可信软件体系结构设计方法

近年来,软件的可信性成为软件质量的焦点,对软件可信性的分析、度量和应用支撑成为热点问题.对软件实施有效的监控是提升软件可信性的一种重要途径.然而目前的研究工作主要集中在软件编码以及相关技术的实现层,缺乏一套系统的软件体系结构设计方法以指导、支持运行监控的可信软件的分析和设计.通过引入面向侧面的软件体系结构设计方法及其相关概念,文中提出一种支持运行监控的可信软件体系结构设计方法.在支持运行监控的可信软件构造模型TSCM的基础上,利用一种面向侧面的体系结构描述语言AC2-ADL描述具有监控能力的软件体系结构,试图为分析和设计具有监控能力的系统的软件体系结构提供一种有效的解决方案.通过结合网上拍卖系统的案例展示该方法的主要步骤和结果,讨论了研究中存在的问题和进一步的工作.     

一个面向方面的可信软件开发平台TSCE*

随着软件规模和复杂度的增加,软件失效和故障问题日益加剧。如何在开发阶段利用开发环境为实现软件可信性提供有效支撑,从而确保软件运行行为与预期保持一致,具有重要的研究价值。借助面向方面的设计思想,把可信性作为一种方面融入软件的开发环境,研究实现了可信软件开发平台TSCE。该平台能够在软件研制过程中,一体化地提供可信性需求定制、可信代码自动生成、可信代码自动织入等辅助开发手段。利用该平台,开发人员不用额外编写可信性实现的相关代码,便可在部署运行阶段使软件具有一定的可信性判断能力和故障预警与修复能力。     

VERTAF: an application framework for the design and verification of embedded real-time software

The growing complexity of embedded real-time software requirements calls for the design of reusable software components, the synthesis and generation of software code, and the automatic guarantee of nonfunctional properties such as performance, time constraints, reliability, and security. Available application frameworks targeted at the automatic design of embedded real-time software are poor in integrating functional and nonfunctional requirements. To bridge this gap, we reveal the design flow and the internal architecture of a newly proposed framework called verifiable embedded real-time application framework (VERTAF), which integrates software component-based reuse, formal synthesis, and formal verification. A formal UML-based embedded real-time object model is proposed for component reuse. Formal synthesis employs quasistatic and quasidynamic scheduling with automatic generation of multilayer portable efficient code. Formal verification integrates a model checker kernel from SGM, by adapting it for embedded software. The proposed architecture for VERTAF is component-based and allows plug-and-play for the scheduler and the verifier. Using VERTAF to develop application examples significantly reduced design effort and illustrated how high-level reuse of software components combined with automatic synthesis and verification can increase design productivity.     

Automatic synthesis and verification of real-time embedded software for mobile and ubiquitous systems

Currently available application frameworks that target the automatic design of real-time embedded software are poor in integrating functional and non-functional requirements for mobile and ubiquitous systems. In this work, we present the internal architecture and design flow of a newly proposed framework called Verifiable Embedded Real-Time Application Framework (VERTAF), which integrates three techniques namely software component-based reuse, formal synthesis, and formal verification. Component reuse is based on a formal unified modeling language (UML) real-time embedded object model. Formal synthesis employs quasi-static and quasi-dynamic scheduling with multi-layer portable efficient code generation, which can output either real-time operating systems (RTOS)-specific application code or automatically generated real-time executive with application code. Formal verification integrates a model checker kernel from state graph manipulators (SGM), by adapting it for embedded software. The proposed architecture for VERTAF is component-based which allows plug-and-play for the scheduler and the verifier. The architecture is also easily extensible because reusable hardware and software design components can be added. Application examples developed using VERTAF demonstrate significantly reduced relative design effort as compared to design without VERTAF, which also shows how high-level reuse of software components combined with automatic synthesis and verification increases design productivity.     

Experience with logical code analysis in software maintenance

Formal program specification and logical analysis are often used for program derivation and proofs of correctness. The basic tools include the logic of predicate calculus and Dijkstra's weakest precondition calculations. Recent work has shown that these tools are also very useful in the maintenance phase of the software life-cycle. This paper reports experience working with software maintenance teams to apply formal methods. Formal logical analysis is invaluable for isolating defects, determining code corrections, eliminating side-effects, and code re-engineering. Logical analysis works well in software maintenance because many defects can be isolated to small segments of code. These small segments can then be analyzed manually or with code analysis tools. The result is lowered software maintenance costs due to the benefits of defect prevention, reduction of code complexity metrics, productivity improvements, and better specifications and documentation. It would be beneficial to use logical code analysis in the earlier phases of the software life-cycle, such as quality assurance and inspection.     

Executable formal specifications of complex distributed systems with CoreASM

Formal specifications play a crucial role in the design of reliable complex software systems. Executable formal specifications allow the designer to attain early validation and verification of design using static analysis techniques and accurate simulation of the runtime behavior of the system-to-be. With increasing complexity of software-intensive computer-based systems and the challenges of validation and verification of abstract software models prior to coding, the need for interactive software tools supporting executable formal specifications is even more evident. In this paper, we discuss how CoreASM, an environment for writing and running executable specifications according to the ASM method, provides flexibility and manages the complexity by using an innovative extensible language architecture.     

Improving the efficiency of automated protocol implementation using Estelle

Correctness and runtime efficiency are essential properties of software in general and of high-speed protocols in particular. Establishing correctness requires the use of FDTs during protocol design, and to prove the protocol code correct with respect to its formal specification. Another approach to boost confidence in the correctness of the implementation is to generate protocol code automatically from the specification. However, the runtime efficiency of this code is often insufficient. This has turned out to be a major obstacle to the use of FDTs in practice. One of the FDTs currently applied to communication protocols is Estelle. We show how runtime efficiency can be significantly improved by several measures carried out during the design, implementation and runtime of a protocol. Recent results of improvements in the efficiency of Estelle-based protocol implementations are extended and interpreted.     

Integrated static code analysis and runtime verification

Static code analysis tools automatically generate alerts for potential software faults that can lead to failures. However, these tools usually generate a very large number of alerts, some of which are subject to false positives. Because of limited resources, it is usually hard to inspect all the alerts. As a complementary approach, runtime verification techniques verify dynamic system behavior with respect to a set of specifications. However, these specifications are usually created manually based on system requirements and constraints. In this paper, we introduce a noval approach and a toolchain for integrated static code analysis and runtime verification. Alerts that are generated by static code analysis tools are utilized for automatically generating runtime verification specifications. On the other hand, runtime verification results are used for automatically generating filters for static code analysis tools to eliminate false positives. The approach is illustrated for the static analysis and runtime verification of an open‐source bibliography reference manager software. Copyright © 2014 John Wiley & Sons, Ltd.     

Discovering Documentation for Java Container Classes

Modern programs make extensive use of reusable software libraries. For example, we found that 17 percent to 30 percent of the classes in a number of large Java applications use the container classes from the java.util package. Given this extensive code reuse in Java programs, it is important for the reusable interfaces to have clear and unambiguous documentation. Unfortunately, most documentation is expressed in English and, therefore, does not always satisfy these requirements. Worse yet, there is no way of checking that the documentation is consistent with the associated code. Formal specifications present an alternative that does not suffer from these problems; however, formal specifications are notoriously hard to write. To alleviate this difficulty, we have implemented a tool that automatically derives documentation in the form of formal specifications. Our tool probes Java classes by invoking them on dynamically generated tests and captures the information observed during their execution as algebraic axioms. Although the tool is not complete or correct from a formal perspective, we demonstrate that it discovers many useful axioms when applied to container classes. These axioms then form an initial formal documentation of the class they describe.     

Developing and evolving a DSL-based approach for runtime monitoring of systems of systems

Complex software-intensive systems are often described as systems of systems (SoS) due to their heterogeneous architectural elements. As SoS behavior is often only understandable during operation, runtime monitoring is needed to detect deviations from requirements. Today, while diverse monitoring approaches exist, most do not provide what is needed to monitor SoS, e.g., support for dynamically defining and deploying diverse checks across multiple systems. In this paper we report on our experiences of developing, applying, and evolving an approach for monitoring an SoS in the domain of industrial automation software, that is based on a domain-specific language (DSL). We first describe our initial approach to dynamically define and check constraints in SoS at runtime and then motivate and describe its evolution based on requirements elicited in an industry collaboration project. We furthermore describe solutions we have developed to support the evolution of our approach, i.e., a code generation approach and a framework to automate testing the DSL after changes. We evaluate the expressiveness and scalability of our new DSL-based approach using an industrial SoS. We also discuss lessons we learned. Our results show that while developing a DSL-based approach is a good solution to support industrial users, one must prepare the approach for evolution, by making it extensible and adaptable to future scenarios. Particularly, support for automated (re-)generation of tools and code after changes and automated testing are essential.     

基于定理证明的内存安全性动态检测算法的正确性研究

随着软件运行时验证技术的发展,出现了许多面向C语言的运行时内存安全验证工具。这些工具大多是基于源代码或者中间代码插桩技术来实现内存安全的运行时检测。但是,其中一些没有经过严格证明的验证工具往往存在两方面的问题,一是插桩程序的加入可能会改变源程序的行为及语义,二是插桩程序并不能有效保证内存安全。为了解决这些问题,文中提出了一种使用Coq定理证明器来判定内存安全验证工具算法是否正确的形式化方法,并使用该方法对C语言运行时验证工具Movec的动态检测算法的正确性进行了证明。对安全规范性质的证明结果表明了Movec的内存安全性动态检测算法是正确的。