Model based testing in incremental system development

The spiraling nature of evolutionary software development processes produces executable parts of the system at the end of each loop. It is argued that these parts should consist not only of programming language code, but of executable graphical system models. As a main benefit of the use of more abstract, yet formal, modeling languages, a method for model based test sequence generation for reactive systems on the grounds of Constraint Logic Programming as well as its implementation in the CASE tool A F is presented.     

基于标记语言的并行多核编程方法

提出一种在多核平台上的快速多线程编程模型ThreadXML。该模型通过使用标记语言形式,提高程序的开发效率,支持可视化,增强并行程序设计的移植性。其中,语言模型编译器的实现采用代码模板技术和面向对象技术相结合的方式,能将ThreadXML源代码转换成目前可执行的程序代码,辅助可视化工具采用图元对象和代码模板技术实现。     

Mediator模型的SystemC代码自动生成

Mediator是一种基于组件的建模语言,该语言主要通过自动机和系统对模型进行描述。将Mediator语言描述的模型自动生成为可执行代码,可以避免编码过程中由于人为疏忽而造成的错误,从而提高编码的可靠性,同时缩短模型开发周期。介绍一种从Mediator模型到SystemC代码的自动生成工具,该工具旨在将基于特定平台的模型转换为能直接仿真运行的代码。首先对Mediator语言的语法语义进行分析,选择合适的SystemC代码组织形式,然后针对Mediator模型的每一个组成部分 设计生成规则,其中重点对类型生成、状态转移语句生成、同步语句的生成进行分析。最后,通过一个机器掉电检测系统说明该工具运行结果的正确性。     

基于XML和ECA规则的工作流建模及执行

长期以来,工作流产品互操作性的缺乏、尤其是工作流建模语言互操作性缺乏,已成为阻碍工作流技术进一步发展的重要因素,XML作为万维网组织规定的结构化的标记语言,它可以用作描述过程模型的共同语法格式,有望解决工作流描述语言的互操作性问题。文章介绍了采用基于XML的工作流描述语言XFL及其工作流管理系统XFMS。由于XFL本身并不是可执行模型,XFMS系统在低层采用了基于规则的工作流执行系统。并给出了从XFL语言到ECA规则的映射方式,所采用的方法综合了面向规则系统的灵活性以及基于XML模型的可交换性和易学性。     

On the automated translational execution of the action language for foundational UML

To manage the rapidly growing complexity of software development, abstraction and automation have been recognised as powerful means. Among the techniques pushing for them, model-driven engineering has gained increasing attention from industry for, among others, the possibility to automatically generate code from models. To generate fully executable code, models should describe complex behaviours. While pragmatically this is achieved by employing programming languages for defining actions within models, the abstraction gap between modelling and programming languages can undermine consistency between models and code as well as analysability and reusability of models. In light of this, model-aware action languages should be preferred. This is the case of the Action Language for Foundational UML (ALF). In this paper, we provide a solution for the fully automated translational execution of ALF towards C++. Additionally, we give an insight on how to simplify the transition from the use of programming languages for modelling fine-grained behaviours to model-aware action languages in industrial MDE. The solution presented in this paper has been assessed on industrial applications to verify its applicability to complex systems as well as its scalability.     

Modeling complex spoken dialog

We develop a commercial phone-based SDS (spoken dialog system) that supplies information to employees about their holiday-allowance. Frequently-asked-questions (FAQ) system use of the conceptual dialog language (CDL), a customized language that express patterns specific to the system's dialog model while still providing a clear picture of the dialog model to domain experts and supporting model updates. CDL's power stems from its ability to capture the specifics of an SDS application while remaining flexible enough to support a range of modeling styles and requirements. To facilitate effective communication with domain experts, modelers can translate the dialog model in CDL to an HTML document, or they can compile it to a programming language for executable code.     

A generic framework for representing and analyzing model concurrency

Software and Systems Modeling - Recent results in language engineering simplify the development of tool-supported executable domain-specific modeling languages (xDSMLs), including editing (e.g.,...     

Designing and prototyping data-intensive applications in the Logresand Algres programming environment

The authors present an environment and a methodology for the design and rapid prototyping of data-intensive software applications, i.e., applications which perform substantial retrieval and update activity on persistent data. In the approach, the application is formally specified using Logres, a database language which combines object-oriented data modeling and rule-based programming. These specifications are translated into Algres, an extended relational algebra, thus yielding a rapid executable prototype. Algres programs embedded into a conventional programming language interface may be converted to conventional programs operating on a commercial relational system. This methodology helps automate the conversion from declarative requirements to imperative code, performing several tasks fully automatically and reducing the probability of human errors, while integrity constraints and application specifications are expressed in a declarative language, at a very high level of abstraction     

A transformation contract to generate aspects from access control policies

Access control is an important security issue. It has been addressed since the late 1960s in the early time-sharing computer systems. Many access control models have been proposed since than but of particular interest is Ferraiolo and Khun’s role-based access control model (RBAC). It is a simple and yet general model which has been deeply studied and applied both in industry and in academia. A variety of industrial standards have been proposed based on this model. Generating code for an access control policy is an interesting challenge. Understanding access control as a non-functional concern that cross-cuts the functional part of a system raises difficulties quite suitable for a solution based on aspect-oriented programming. In this paper, we address the problems of specification and validation of code generation for access control policies targeting an aspect-based infra-structure. We propose an MDA approach. The code generator is a transformation from SecureUML, an RBAC-based modeling language, to the language Aspects for Access Control (AAC), an aspect-oriented modeling language proposed in this paper. Metamodels are used to represent the languages and to specify the transformation. A metamodel is used to represent the abstract syntax of a language and the constraints that a given instance model of the metamodel must fulfill. We also use a metamodel to specify the code generator. This transformation metamodel, together with all the constraints, that is, from both languages and those constraints regarding the merge of the two languages, we call a transformation contract. It merges and conservatively extends the source and target metamodels of the model transformation it represents. In the context of code-generation for access control policies, the transformation contract specifies the relationships between the abstract syntaxes of SecureUML and AAC and constrains the two languages. The validation of the code generator also uses the transformation contract. For a given access control policy and aspect, represented as instances of the appropriate metamodels, with aspects produced by the code generator, the constraints of the transformation contract must hold. We have prototyped a transformer from SecureUML to aspects on top of ITP/OCL, an OCL interpreter that automatically validates the generated aspect code by applying the constraints of the transformation contract.     

Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL

We present a formalization and a formal total correctness proof of a MiniSAT-like SAT solver within the system Isabelle/HOL. The solver is based on the DPLL procedure and employs most state-of-the-art SAT solving techniques, including the conflict-guided backjumping, clause learning, and the two-watched unit propagation scheme. A shallow embedding into Isabelle/HOL is used and the solver is expressed as a set of recursive HOL functions. Based on this specification, the Isabelle’s built-in code generator can be used to generate executable code in several supported functional languages (Haskell, SML, and OCaml). The SAT solver implemented in this way is, to our knowledge, the first fully formally and mechanically verified modern SAT solver.     

Property-driven benchmark generation: synthesizing programs of realistic structure

We present a systematic approach to the automatic generation of platform-independent benchmarks of realistic structure and tailored complexity for evaluating verification tools for reactive systems. The idea is to mimic a systematic constraint-driven software development process by automatically transforming randomly generated temporal-logic-based requirement specifications on the basis of a sequence of property-preserving, randomly generated structural design decisions into executable source code of a chosen target language or platform. Our automated transformation process steps through dedicated representations in terms of Büchi automata, Mealy machines, decision diagram models, and code models. It comprises LTL synthesis, model checking, property-oriented expansion, path condition extraction, theorem proving, SAT solving, and code motion. This setup allows us to address different communities via a growing set of programming languages, tailored sets of programming constructs, different notions of observation, and the full variety of LTL properties—ranging from mere reachability over general safety properties to arbitrary liveness properties. The paper illustrates the corresponding tool chain along accompanying examples, emphasizes the current state of development, and sketches the envisioned potential and impact of our approach.     

An Eclipse-based Integrated Environment for Developing Executable Structural Operational Semantics Specifications

The Structural Operational Semantics Development Tooling (SOSDT) Eclipse Plugin integrates the Relational Meta-Language (RML) compiler and debugger with the Eclipse Integrated Development Environment Framework. SOSDT, together with the RML compiler and debugger, provides an environment for developing and maintaining executable Structural Operational Semantics specifications, including the Natural Semantics big step variant of SOS specifications. The RML language is successfully used at our department for writing large specifications for a range of languages like Java, Modelica, Pascal, MiniML etc. The SOSDT environment includes support for browsing, code completion through menus or popups, code checking, automatic indentation, and debugging of specifications.     

Using UML Action Semantics for model execution and transformation

The Unified Modelling Language (UML) lacks precise and formal foundations and semantics for several modeling constructs, such as transition guards or method bodies. These semantic discrepancies and loopholes prevent executability, making early testing and validation out of reach of UML tools. Furthermore, the semantic gap from high-level UML concepts to low-level programming constructs found in traditional object-oriented language prevents the development of efficient code generators.The recent Action Semantics (AS) proposal tackles these problems by extending the UML with yet another formalism for describing behavior, but with a strong emphasis on dynamic semantics. This formalism provides both, a metamodel integrated into the UML metamodel, and a model of execution for these statements. As a future OMG standard, the AS eases the move to tool interoperability, and allows for executable modeling and simulation.We explore in this paper a specificity of the AS: its applicability to the UML metamodel, itself a UML model. We show how this approach paves the way for powerful metaprogramming for model transformation. Furthermore, the overhead for designers is minimal, as mappings from usual object-oriented languages to the AS will be standardized.     

一种同步语言多线程代码自动生成工具

随着安全关键系统对计算性能要求的日趋提高,能够提供更强计算能力而又减少电子设备的体积、重量和功耗的多核处理器将在安全关键领域得到广泛应用.同步语言能够表达确定性并发行为且具有精确时间语义等特性,适用于安全关键软件的建模和验证.目前,同步语言SIGNAL编译器主要支持串行代码生成,较少关注多线程代码生成.提出一种同步语言SIGNAL多线程代码生成工具.首先将SIGNAL程序转换为经过时钟演算的S-CGA中间程序;之后将S-CGA中间程序转换为时钟数据依赖图以分析依赖关系;然后对时钟数据依赖图进行拓扑排序划分,并针对划分结果提出优化算法和基于流水线方式的任务划分方法;最后将划分结果转换为虚拟多线程结构并进一步生成可执行多线程C/Java代码.通过在多核处理器上的实验,验证了所提方法的有效性.     

基于Petri网的SysML活动图的分析与验证

系统建模语言(Systems Modeling Language,SysML)是目前国际上系统工程领域最新的标准建模语言,它包括语义和表示法两部分,缺乏分析和验证的手段。为了弥补这一不足,研究了SysML活动图到Petri网的转换方法,主要定义了将SysML活动图转换为相应Petri网可执行模型的6种转换规则。应用这些规则可以将活动图转换为Petri网模型,进而对其进行化简、分析和验证,同时可检测SysML的行为规范与并发相关的性质,如死锁、有界性等。采用列举法和模拟法验证了所建模型的一致性。证书申请活动图的实例表明,该方法是可行的。     

Generating tools from graph-based specifications

This paper describes an approach for generating graphical, structure-oriented software engineering tools from graph-based specifications. The approach is based on the formal meta modeling of visual languages using graph rewriting systems. Besides the syntactical and semantical rules of the language, these meta models include knowledge from the application domains. This enables the resulting tools to provide the user with high level operations for editing, analysis and execution of models. Tools are constructed by generating source code from the meta model of the visual language, which is written in the very high level programming language PROGRES. The source code is integrated into a framework which is responsible for the invocation of commands and the visualization of graphs. As a case study, a visual language for modeling development processes together with its formal meta model is introduced. The paper shows how a process management tool based on this meta model is generated and reports on our experiences with this approach.