SPIN's Promela转Java编译器：Stratego的助力研究

需积分: 10 178 浏览量更新于2024-07-17 收藏 1.28MB PDF 举报

本论文主要探讨了"SPIN's Promela to Java Compiler"这一创新工具，该工具是在Stratego的帮助下开发的。SPIN是一种流行的模型检查框架，它允许系统工程师构建和验证软件系统的形式化模型，以便检测潜在的错误和不符合规格的行为。然而，尽管模型检查提供了一种强大的验证手段，实际将这些模型转化为可执行的应用程序代码仍然是一项繁琐的任务，因为缺乏自动化工具。 Edwin Vielvoije撰写了他的硕士论文，研究的主题正是如何利用Stratego的强大功能，将SPIN的Promela语言编写的模型自动转换为Java代码。Promela是SPIN的核心语言，它结合了过程式的编程风格和离散事件系统建模的特点，常用于描述并发和交互行为。Stratego，作为一种高级程序变换工具，以其强大的模式匹配和策略驱动的文本处理能力著称。论文的核心内容涉及Promela到Java编译器的设计与实现，它旨在解决从模型设计阶段跨越到实际编程阶段的桥梁问题。通过这种编译器，用户可以利用SPIN的建模能力，然后直接生成符合Java语法的代码，从而显著减少手动编码的工作量，提高软件开发的效率和生产力。论文作者Edwin Vielvoije详细介绍了编译器的工作原理，包括如何解析Promela语法，映射模型结构到Java代码，以及处理可能遇到的复杂逻辑和数据结构转换。他还讨论了在设计过程中遇到的挑战，如保持语义一致性、处理并发特性，以及如何优化生成的Java代码性能。此外，论文还可能涵盖了性能评估、工具的适用性和局限性，以及与现有技术的比较分析。对于那些致力于模型驱动开发和自动代码生成的软件工程研究者来说，这项工作具有重要的理论价值和实践意义，因为它展示了如何通过巧妙地结合两种不同的工具和技术来简化软件开发流程。这篇论文为SPIN用户提供了将模型直接转化为Java代码的新途径，推动了模型检查和自动代码生成技术的边界，对于提升软件质量与开发效率具有重要意义。

1.1 Research Introduction

that are created in MDA. If those languages and tools could help me in creating such a

transformation, then MDA could be used for this project. I also wanted to know what

already has been done in other research about transforming the Promela language into some

other language and how this would translate to certain Java properties. I needed to ﬁnd a

certain solution for the parts of which there was no known transformation as well.

Model Driven Architecture

An MDA design consists of a Platform Independent Model or PIM, that describes a sys-

tem or application without dependencies on any platform. A platform can be anything

from a programming language to hardware to an operating system. A PIM would then be

transformed into a Platform Speciﬁc Model or PSM, which still describes the system or

application but now the design is speciﬁc to a certain platform on which the system or ap-

plication will eventually be realized. A PSM would then be transformed into actual source

code to create the actual system or application. The PIM and PSM can be written in dif-

ferent or the same languages and all transformations between the different models are done

automatically via (MDA) tools. An overview can be found in Figure 1.1.

Figure 1.1: The MDA models and their relation

If MDA would be used for this project then a Platform Independent Model (PIM) should

be created that describes the Promela language independent from any platform, such as any

programming language, operating system or hardware. This PIM should then be trans-

formed automatically via (MDA) tools into a Platform Speciﬁc Model (PSM), which in this

case would be speciﬁc to the Java language. The derived PSM should then be transformed

into source code, which in this case would be Java code [24]. This Java code should then be

used as a framework of which each Promela model would depend on after its transformation

to Java.

UML

My research [30] indicated that UML [6, 7, 12] probably is the most widely known and

most commonly used modeling language. UML consists of a number of different diagrams.

Introduction 1.1 Research

The most import models are the class, sequence, state-machine and use case diagrams.

The SPIN program creates a state-machine from a Promela model to verify the require-

ments of the system that is modeled [17, 19]. A state-machine diagram can be created

easily of a Promela model. The state-machine will cover every possible way of executing

the model, just as SPIN does. However, this will end up in a state-machine diagram with a

lot of states. The bigger the Promela model is, the larger the amount of states will be in the

diagram. This diagram shows how the model behaves, but does not show the components

the model consists of.

One could try creating a class diagram corresponding to a Promela model by listing

the processes and channels as classes in the diagram and the variables as attributes in the

classes. There should then always be an extra class to contain all the global variables and

the previously described channels. The processes can access that class to gain information

about the global variables or change them and send or receive from the declared channels.

This diagram can be used to show what parts the model consists of, but does not show

anything at all about the behavior.

A sequence diagram of a Promela model is a bit like a simulated run in SPIN. The

veriﬁcation will take all paths whilst the simulation only takes one path [17, 19]. In this

way a sequence diagram cannot show all the possible behavior of a model or sometimes

not even all the components of the model. A sequence diagrams can be created for every

possible path in the model. All of those sequence diagrams together show all the behavior

and all the components that are used in the model. However, as with the state-machine

diagram, the number of paths is large and will be even larger when a model grows bigger.

A use case diagram can be created for a Promela model. The processes will then be

the actors and the use cases will then describe an action the process will undertake. The

use cases follow each other in the same way the actions follow each other in the Promela

model. The use case diagram shows the behavior of the separate processes but not how

those processes interact. These diagrams do not show when which process executes which

actions.

Action Semantics

UML is not a good choice to use as a language for the PIM because UML is not able

to show the non-deterministic and interleaving nature of the Promela language. Action

Semantics [25] did show promise to be used instead.

Action semantics can be used to describe a programming language. In [25] a complete

description can be found on Action Semantics. There is no graphical representation for any

part of the Action Semantics, it only consists of formulas. When Action Semantics are used

to describe a language, then three parts need to be created. Those three parts are an abstract

syntax, semantic functions and semantic entities. These three parts together can be used

to describe a programming language. These descriptions could be used as a PIM in this

project.

The abstract syntax provides as described in [25] “an appropriate interface between the

concrete syntax and the semantics”. An abstract syntax can most of the time be obtained by

looking at parse tree structures and leave out those details which have no semantic signiﬁ-

Introduction 1.1 Research

Promela2Java Compiler

When you read a book or article about compiler construction, such as [15], then you know

that a compiler mainly consist out of three parts. The front-end, the semantic representation

and the back-end. The front-end of the compiler analyzes the program in the language that

needs to be compiled, in this case Promela models. The back-end creates a program in the

target language, which is in this case Java. The semantic representation glues both parts

together. The output of the front-end is an abstract syntax tree of the input program. The

semantic representation part of the compiler takes that abstract syntax tree and constructs

intermediate code. Finally, the back-end takes the intermediate code and generates the code

in the target language.

I showed in [30] as well that the transformation from a Promela model to Java code

could be done by creating a compiler with the Stratego/XT toolset [9, 31]. With this toolset

a parser, a transformation and code generator (or pretty-printer) can be created from a gram-

mar and transformation rules written by a user. These three parts are practically equal to

the parts of the compiler. The created parser represents the front-end of the compiler, whilst

the transformation rules represent the semantic representation part of a compiler and the

back-end is represented by the code generator. A separate package for the toolset is even

able to understand parts of the Java language, which could be very helpful because the tar-

get language of the compiler that needs to be created is the Java language. More on how

Stratego works can be found further on in this chapter.

Promela to Java Transformations

Information that showed up during my research [30] were some Promela to Java transfor-

mations that could be used to create a compiler. All these transformations can be found

in the Table 1.1, the left column shows the Promela part and the right column shows what

those parts should transform to in Java or what kind of construction could help facilitate the

Promela part in Java.

Promela Java

Processes Threads

Variables Variables

Data types built-in data types and Classes

d step and atomic Lock interface and the Metalocking algorithm

Channels and Concurrency BlockingQueue and java.util.concurrent

Non-determinism Scheduler chooses a path and speculative execution

Channel operations Methods in subclasses of BlockingQueue

Labels and goto Loop and switch statement

unless statement Executable checks and if statements

Embedded C code No translation

Table 1.1: Promela to Java translations

剩余81页未读，继续阅读

jiangdmdr

粉丝: 58
资源: 764

SPIN's Promela转Java编译器：Stratego的助力研究

Introduction to SPIN & Promela

spin和promela简介

From NuSMV to SPIN Experiences with model checking.pdf

并发系统Promela建模、SPIN的使用

并发系统的Promela语言建模与SPIN模型检测

SPIN与Promela模型检测入门

使用SPIN和PROMELA设计与验证通信协议实战教程

SPIN-to-GRAPE：Promela模型分析与对称性简化工具

并发系统分析：Promela建模与SPIN模型检测实践

在使用SPIN和Promela进行并发系统模型检测时，如何有效地应对状态空间爆炸问题？请结合具体实践案例说明。

最新资源