基于面向特征编程范式的形式化验证技术的应用与研究

本文系统详尽阐述了FOP编程范式的思想,通过类比,指出FOP与面向方面编程范式的异同。同时还说明FOP给形式化验证技术带来的挑战。本文还比较了现有的FOP形式化验证方法以及我们所做的相关工作的优缺点,并对FOP形式化验证今后可能的研究和发展方向进行讨论。     

应用面向特征编程方法FOP实现软件产品线增量开发

面向对象编程OOP(Object Oriented Programming)技术在实现软件产品线时存在不足,一个重要原因是OOP对产品线可变性的支持有限.在OOP的基础上,相关研究者提出面向特征编程FOP(Feature Oriented Programming),研究特征的模块性,以及支持特征模块性的编程模型.本文对FOP的相关技术和模型进行了研究,提出基于FOP进行软件产品线的增量开发,可以实现产品线更高层次的模块化和特征的灵活配王,同时避免了维护困难.在此基础上对一个网上缴费产品线实例进行研究,实现和验证了相关方法和结论.最后基于实验对FOP的优缺点进行了讨论.     

基于着色Petri网构建AFM范式的形式化模型AFM-CPN

针对重用已有的软件模型与资源高效地开发软件的要求,软件产品线编程范式是一种可行的解决方案。方面化特征模块AFM(Aspectual Feature Module)编程范式是一种最新提出的软件产品线编程范式,它引入了AOP编程范式,将系统基于特征而非角色划分能够获得重用性更强的设计。Petri网能够利用一种图形化的表示方法进行系统建模,而且提供理论上的验证机制。把Petri网引入到AFM范式当中,这样既可以根据迭代的方式构建所需的AFM模块以降低建模的规模和复杂度,也可以利用Petri网来实现AFM范式的形式化验证。     

基于层次状态机的方面化特征模块的增量式验证

方面化特征模块(AFM)是最新提出的软件产品线(SPL)编程范式,能解决现有SPL编程范式存在的问题,但由于AFM范式同时存在模块的并发组合和顺序组合,现有的组合验证技术和模块化模型检验技术并不适用于AFM程序的验证,且目前还未见到针对AFM的验证方法,这制约了AFM范式的应用.文中首次为AFM范式建立了形式化模型,并基于此模型提出一种AFM程序的增量式的验证方法.该方法可以从一个小规模的AFM程序的验证开始,以后每次只添加对新组合的AFM模块的验证,因此可避免直接验证大型AFM程序时可能由于模型的规模太大而无法验证的问题.     

面向特征的编程研究与实践

面向对象的编程已深入人心,但实现贯穿于多个对象的复杂特征功能时,表现不佳。针对其不足,面向特征的编程(FOP)提供了一种组织代码的不同的方法,通过对原型系统不断地修改添加新的特征直到系统演化成熟,增强了面向对象的性能,使得代码的定义、测试、修改和组织更加清晰,是逐步求精开发方法的一个重要编程方法。介绍面向特征编程的理论基础及其实现工具,对相关技术及模型进行研究,并通过具体实例展示了面向特征编程的易配置、易演化和易维护的特点。     

面向特征编程中的特征组合失效问题及其解决方法

软件产品线的特征之间存在依赖关系,因此在面向特征编程(FOP)中,特征模块之间在代码结构上存在密切关联.另一方面,具有可变性的特征在应用产品中的绑定与否会对依赖关系的实现造成破坏性的影响,导致FOP在实施过程中可能出现特征组合失效问题.对该问题的产生进行分析,总结出3种主要的依赖场景.另外,提出一种特征模块垂直分解方法,其核心机制在于将可变性引入特征模块内部,根据需求组装实现代码,从而可避免出现组合失效问题.最后,通过一个出版社利润考核系统产品线实例验证了方法的有效性.     

面向Agent软件工程研究现状与展望

文章介绍了面向Agent软件工程(AOSE)的关键抽象集,综述了形式化和非形式化AOSE方法、Agent统一模型语言(AUML)、AOSE开发工具的研究现状和存在的主要问题,最后根据面向Agent编程范型表示一种计算的社会观点,基于社会学理论展望了AOSE的下一步发展。     

面向方面软件动态耦合的度量

耦合性是两个模块间相互作用的测度。面向方面编程是一种新的编程范型,它支持关注点的分离。目前,对于面向方面软件耦合度量的常用方法是对软件进行结构分析和静态代码分析。然而,由于系统中的动态绑定以及代码中大量无用的方面代码导致静态度量结果无法精确地反映程序运行时的实际耦合。首先提出适用于面向方面软件的动态耦合度量框架。接着,在该框架的基础上,根据不同的耦合关系类型,形式化定义了动态耦合度量指标集,并验证数学属性。最后,讨论了动态耦合度量工具的实现。     

面向儿童的图形化编程语言和工具

针对现有的面向儿童的编程工具在图形化表示、交互设计等方面存在的不足,以及没有专门面向中国儿童的编程工具的问题,提出一种面向儿童的图形化编程范式和图形语言的描述方式,设计实现了适合8～14岁中国儿童使用的图形化编程语言和编程工具.以儿童用户的特点为核心,设计了10类图形化编程块,从逻辑层、物理层和数据接口层对编程块的属性进行多元组描述;根据图形化编程块的形状语义和功能定义图形化编程语言的语法规则,采用笔式交互技术为儿童设计实现了一个简单易用的编程工具,最后通过2个实例并结合初步用户评估实验,验证了该图形化编程工具的可用性.     

一种基于CSP的面向方面状态图形式化描述方法

面向方面通过分离关注点解决软件系统中的横切问题,通过扩展UML可实现对面向方面的建模。本文利用UML的扩展机制将方面加入状态图中,描述了状态图中的方面与核心组件以及方面之间的编织,然后利用进程代数的形式化语义描述了扩展后的UML状态图,克服了扩展UML描述状态图的缺乏形式化动态语义,不利于对模型进行形式化验证和证明的缺
点。最后,以ATM自动取款机为例验证了基于CSP的面向方面状态图形式化描述的有效性。     

LSC Verification for UML Models with Unbounded Creation and Destruction

The approaches to automatic formal verification of UML models known up to now require a finite bound on the number of objects existing at each point in time. In [W. Damm, B. Westphal, Live and let die: LSC-based verification of UML-models, Science of of Computer Programming 55 (2005) 117–159] we have observed that the class of hardware systems with replicated components studied by McMillan [K.L. McMillan, A methodology for hardware verification using compositional model checking, Science of Computer Programming 37 (2000) 279–309] is equivalent to the class of systems where the only source of infiniteness is unbounded creation and destruction of objects, i.e. where all data-types except for object identities are finite. Exploiting the symmetry of UML models induced by objects being instances of classes, the restriction to finite bounds can be overcome applying [K.L. McMillan, A methodology for hardware verification using compositional model checking, Science of Computer Programming 37 (2000) 279–309].In this paper we report on experiences from an evaluation of this approach within the UML Verifi- cation Environment (UVE) [I. Schinz, T. Toben, C. Mrugalla and B. Westphal, The Rhapsody UML Verification Environment, in: J.R. Cuellar and Z. Liu, editors, Proceedings SEFM 2004 (2004), pp. 174–183], a state-of-the-art tool for formal verification of UML models using Live Sequence Charts (LSC) [W. Damm, D. Harel, LSCs: Breathing Life into Message Sequence Charts, Formal Methods in System Design 19 (2001) 45–80] for requirements specification.     

基于代数-时态逻辑的象形对象研究

本文首先讨论了国内外有关面向对象方法学、代数规范、时态逻辑的研究现状 ,分析了对象形式化语义研究的不足 .其次 ,分析了几种主要的系统形式化模型和方法 .然后 ,在我们已研究的“计算机甲骨文象形码输入法”的基础上 ,从时态逻辑的角度定义了象形对象及其约束条件 ,定义了面向对象的有色 Petri网 (OOPEN) ,并应用 OOPEN描述了象形对象的层次结构 .最后 ,我们将代数规范与时态逻辑相结合 ,对象形对象的语义基础进行了一些研究 .     

面向方面软件重构等价性形式化证明方法

软件重构在不改变程序行为的情况下通过对代码进行小的改进以提升设计,使之更容易理解和维护,面向方面的程序设计是软件开发的新技术,为了有效实施面向方面的软件重构,需要开发者识别面向方面程序的转化规则。然而,由于使用的AOP语言没有形式化的语义定义,难以确认转化和重构的程序运行行为。本文对MCI操作语义的面向方面的扩展使之支持程序的方面特征的描述,定义了两个程序的观测等价,讨论了AspectJ的形式语义模型的建立,在MCI的语义下形式化地精确证明了Add Before-executing编程规则的观测等价性,其基本原理和方法可以适用于其他规则的证明,通过上述工作提出了面向方面重构的程序和它的面向对象程序原型等价性的证明方法。     

Combining Software and Hardware Verification Techniques

Combining verification methods developed separately for software and hardware is motivated by the industry's need for a technology that would make formal verification of realistic software/hardware co-designs practical. We focus on techniques that have proved successful in each of the two domains: BDD-based symbolic model checking for hardware verification and partial order reduction for the verification of concurrent software programs. In this paper, we first suggest a modification of partial order reduction, allowing its combination with any BDD-based verification tool, and then describe a co-verification methodology developed using these techniques jointly. Our experimental results demonstrate the efficiency of this combined verification technique, and suggest that for moderate–size systems the method is ready for industrial application.     

A formal methodology for integral security design and verification of network protocols

In this work we propose a methodology for incorporating the verification of the security properties of network protocols as a fundamental component of their design. This methodology can be separated in two main parts: context and requirements analysis along with its informal verification; and formal representation of protocols and the corresponding procedural verification. Although the procedural verification phase does not require any specific tool or approach, automated tools for model checking and/or theorem proving offer a good trade-off between effort and results. In general, any security protocol design methodology should be an iterative process addressing in each step critical contexts of increasing complexity as result of the considered protocol goals and the underlying threats. The effort required for detecting flaws is proportional to the complexity of the critical context under evaluation, and thus our methodology avoids wasting valuable system resources by analyzing simple flaws in the first stages of the design process. In this work we provide a methodology in coherence with the step-by-step goals definition and threat analysis using informal and formal procedures, being our main concern to highlight the adequacy of such a methodology for promoting trust in the accordingly implemented communication protocols. Our proposal is illustrated by its application to three communication protocols: MANA III, WEP's Shared Key Authentication and CHAT-SRP.     

Guaranteeing functional safety: design for provability and computer-aided verification

When autonomous robots begin to share the human living and working spaces, safety becomes paramount. It is legally required that the safety of such systems is ensured, e.g. by certification according to relevant standards such as IEC 61508. However, such safety considerations are usually not addressed in academic robotics. In this paper we report on one such successful endeavor, which is concerned with designing, implementing, and certifying a collision avoidance safety function for autonomous vehicles and static obstacles. The safety function calculates a safety zone for the vehicle, depending on its current motion, which is as large as required but as small as feasible, thus ensuring safety against collision with static obstacles. We outline the algorithm which was specifically designed with safety in mind, and present our verification methodology which is based on formal proof and verification using the theorem prover Isabelle. The implementation and our methodology have been certified for use in applications up to SIL 3 of IEC 61508 by a certification authority (TüV Süd Rail GmbH, Germany). Throughout, issues we recognized as being important for a successful application of formal methods in robotics are highlighted. Moreover, we argue that formal analysis deepens the understanding of the algorithm, and hence is valuable even outside the safety context.     

Modeling and formal verification of embedded systems based on a Petri net representation

In this paper we concentrate on aspects related to modeling and formal verification of embedded systems. First, we define a formal model of computation for embedded systems based on Petri nets that can capture important features of such systems and allows their representation at different levels of granularity. Our modeling formalism has a well-defined semantics so that it supports a precise representation of the system, the use of formal methods to verify its correctness, and the automation of different tasks along the design process. Second, we propose an approach to the problem of formal verification of embedded systems represented in our modeling formalism. We make use of model checking to prove whether certain properties, expressed as temporal logic formulas, hold with respect to the system model. We introduce a systematic procedure to translate our model into timed automata so that it is possible to use available model checking tools. We propose two strategies for improving the verification efficiency, the first by applying correctness-preserving transformations and the second by exploring the degree of parallelism characteristic to the system. Some examples, including a realistic industrial case, demonstrate the efficiency of our approach on practical applications.     

A blended E-learning experience in a course of object oriented programming fundamentals

In this paper, we present a blended e-learning experience consisting of supplying an undergraduate student population (in addition to traditional on-site classes) with a learning tool called OOPS (Object Oriented Programming System) and a testing system called SIETTE. OOPS is a problem-solving environment in which students can resolve Object Oriented Programming exercises. The system applies an assessment for learning strategy where students are formatively assessed, i.e. OOPS diagnoses their knowledge level but also generates feedback and hints to help students to understand and overcome their misconceptions and to reinforce correctly learnt concepts. In conjunction with OOPS, we have used SIETTE, a web-based assessment system in which students can take tests and teachers can construct them Subsequently, we have explored whether or not the use of OOPS contributes to improve the students’ knowledge about Object Oriented Programming.     

An empirical research agenda for understanding formal methods productivity

ContextFormal methods, and particularly formal verification, is becoming more feasible to use in the engineering of large highly dependable software-based systems, but so far has had little rigorous empirical study. Its artefacts and activities are different to those of conventional software engineering, and the nature and drivers of productivity for formal methods are not yet understood.ObjectiveTo develop a research agenda for the empirical study of productivity in software projects using formal methods and in particular formal verification. To this end we aim to identify research questions about productivity in formal methods, and survey existing literature on these questions to establish face validity of these questions. And further we aim to identify metrics and data sources relevant to these questions.MethodWe define a space of GQM goals as an investigative framework, focusing on productivity from the perspective of managers of projects using formal methods. We then derive questions for these goals using Easterbrook et al.’s (2008) taxonomy of research questions. To establish face validity, we document the literature to date that reflects on these questions and then explore possible metrics related to these questions. Extensive use is made of literature concerning the L4.verified project completed within NICTA, as it is one of the few projects to achieve code-level formal verification for a large-scale industrially deployed software system.ResultsWe identify more than thirty research questions on the topic in need of investigation. These questions arise not just out of the new type of project context, but also because of the different artefacts and activities in formal methods projects. Prior literature supports the need for research on the questions in our catalogue, but as yet provides little evidence about them. Metrics are identified that would be needed to investigate the questions. Thus although it is obvious that at the highest level concepts such as size, effort, rework and so on are common to all software projects, in the case of formal methods, measurement at the micro level for these concepts will exhibit significant differences.ConclusionsEmpirical software engineering for formal methods is a large open research field. For the empirical software engineering community our paper provides a view into the entities and research questions in this domain. For the formal methods community we identify some of the benefits that empirical studies could bring to the effective management of large formal methods projects, and list some basic metrics and data sources that could support empirical studies. Understanding productivity is important in its own right for efficient software engineering practice, but can also support future research on cost-effectiveness of formal methods, and on the emerging field of Proof Engineering.