基于特征的软件模型形式化验证技术分类

需积分: 9 3 浏览量更新于2024-07-18 收藏 529KB PDF 举报

"形式化验证技术在软件模型中的特征分类" 这篇学术论文《基于特征的软件模型形式化验证技术分类》探讨了在软件模型开发中如何运用形式化验证方法进行分类。形式化验证是一种确保软件系统在设计阶段就满足预定规格和需求的严格分析方法。在模型驱动工程（Model-Based Engineering, MBE）中，软件模型是核心开发工件，用于描绘系统结构和行为，并可自动生成执行代码。因此，模型中的缺陷很可能会影响到生成的可执行代码。论文作者Sebastian Gabmeyer、Petra Kaufmann和Martina Seidl提出，对软件模型的形式化验证技术进行特征分类有助于更好地理解和比较不同的验证方法。形式化验证技术主要包括模型检查（Model Checking）、定理证明（Theorem Proving）等，它们各自有其特定的优势和限制。 1. **模型检查**：模型检查技术通过自动探索所有可能的状态空间来确定一个系统是否满足特定的性质。这种技术特别适用于检查系统的安全性或并发性问题。然而，状态空间爆炸问题可能限制其在大型复杂系统中的应用。 2. **定理证明**：定理证明技术则是通过逻辑推理来证明软件模型是否符合预定的规范。这种方法可以提供完全的保证，但通常需要人类专家的介入以构造和验证证明。因此，它可能更适合于对正确性要求极高的领域，如航空航天或医疗设备软件。 3. **其他技术**：除了模型检查和定理证明，还有诸如符号执行（Symbolic Execution）、抽象解释（Abstract Interpretation）、约束满足问题（Constraint Satisfaction Problems）等方法。这些技术各有侧重点，如符号执行能处理路径敏感的分析，而抽象解释则在不完整信息下提供系统行为的近似理解。论文中，作者可能进一步讨论了这些技术的特征，如它们处理复杂性、效率、自动化程度以及对用户专业知识的要求。此外，他们可能还分析了如何根据特定项目的需求和资源选择合适的形式化验证技术，并提出了一个综合这些特征的分类框架，以指导软件工程师在MBE实践中做出明智的选择。形式化验证在软件开发中的应用日益广泛，尤其是在安全关键领域，因为它能够提前发现潜在的错误，降低软件缺陷导致的严重后果。因此，对这些验证技术的深入理解和有效分类对于提高软件质量和可靠性至关重要。这篇研究为软件工程社区提供了一种新的视角，以更系统化的方式看待和比较各种形式化验证技术，从而促进软件开发过程的优化。

ISIS RR BIG-TR-2014-1 6

properties, examples of which include, among others, Presburger and bit vector arithmetic, or the theory of

arrays. The satisﬁability modulo decidable ﬁrst-order theories is established by SMT solvers like Z3 [39].

Model Checking

Model checking is an automatic theorem proving technique that proves a proposition valid by exploring

and evaluating all relevant – usually a subset of all possible – interpretations over the product of a set of

ﬁnite domains

× · · · × D

. The proposition is referred to as the speciﬁcation and is usually formulated

in a temporal logic. Applied to the veriﬁcation of hard- and software systems [

], the speciﬁcation

expresses desired or undesired properties of the system and the interpretation corresponds to the valuation

of the system’s variables, whose values are drawn from domains

, · · · , D

. A distinct valuation of the

system’s variables identiﬁes a state of the system and the set of all possible variable valuations that are

reachable from the system’s initial state is referred to as the state space of the system. The state space is

traditionally represented by a Kripke structure, but also by ﬁnite automata and linear transition systems (LTS).

A Kripke structure is a ﬁnite, directed graph whose nodes represent the states of the system. The nodes are

labeled with those atomic propositions that are true in that state. The edges of a Kripke structure represent

transitions between their source and their target node and are unlabeled. In contrast, automata and linear

transition systems label transitions with the system’s operations that trigger the state change. All of them

have in common that they describe execution paths of the system, which are deﬁned as, possibly inﬁnite,

sequences

ρ = s

. . .

of states. We say that a state

is reachable from the initial state

if there exists

a ﬁnite path ρ = s

. . . s

The speciﬁcation is most commonly formulated either with Computation Tree Logic (CTL) [

] or

Linear Temporal Logic (LTL) [

119

]. Both share the same set of temporal operators, namely

(next),

(ﬁnally, also: eventually),

(globally), and

(until). In case of CTL, each occurrence of a temporal operator

must be preceded by a path quantiﬁer, either

(on all paths) or

(on some paths), whereas LTL formulas are

implicitly all-quantiﬁed. Intuitively, the formulas

AX ϕ

AF ϕ

AG ϕ

, and

A ϕUψ

are satisﬁed if, along all paths

that start in the current state,

holds in the next state, in some future state (including the current state), in all

future states (including the current state), and in all states until

holds eventually. It follows that a CTL

formula may explore multiple branches due to the requirement that every temporal operator is path-quantiﬁed,

while an LTL formula branches only once in the state where the evaluation starts.

Temporal formulas describe properties that the system should satisfy and can be categorized into safety,

and liveness properties.

Safety properties are characteristically speciﬁed by

AG ϕ

and describe invariants of

the system [

] that hold in every state on all paths. They assert that “nothing bad” ever happens. Liveness

properties test if “something good” happens eventually or repeatedly and are either of the form

F ϕ

GF ϕ

[

]. Moreover, reachability properties are used to test if there exists a path to a state that eventually

satisﬁes some condition ϕ. They are of the form EF ϕ [13].

To algorithmically verify a system with a model checker the user supplies both a representation of the

system and its speciﬁcation as input. In its simplest form, the model checker ﬁrst builds the state space of

the system and then evaluates the speciﬁcation. If the speciﬁcation is violated, the model checker returns a

counterexample trace that describes paths to states that falsify the speciﬁcation. Otherwise, it informs the

user that the speciﬁcation holds.

Model checking is applicable only to ﬁnite state representations of systems. The state space may, however,

become exorbitantly large, because it grows exponentially with every additional system variable. This

phenomenon is known as the state explosion problem. Reducing the number of states and improving the

Note that there exist two classiﬁcation schemes, namely the safety-liveness [2] and the safety-progress classiﬁcation [30].

ISIS RR BIG-TR-2014-1 7

efﬁciency of the state space’s traversal has been the subject of active research for that past 30 years and still

is. This line of research has brought forth several techniques that pushed the number of feasibly analyzable

states from

and beyond. McMillan [

] proposed the ﬁrst symbolic model checking technique

in an effort to reduce the space required to store an explicit enumeration of all states, and represented

states and transitions with Boolean formulas, which he encoded into (Reduced Ordered) Binary Decision

Diagrams (BDD) [

]. Later, Biere et al. [

] presented bounded model checking (BMC), a symbolic

approach that does not require BDDs. It analyzes execution paths of bounded length, thus, offering an

efﬁcient technique that is sound, yet not necessarily complete. In a different line of research, the framework

of abstract interpretation [

] is employed to represent a set of concrete states by a single abstract state. This

overapproximation is conservative, i.e., if a property holds in the abstract system, it holds in the concrete

system, too. If, however, the property fails in the abstract system, the returned counterexample trace need

not describe a realizable trace in the concrete system. This is due to the overapproximation of the abstract

system that may permit execution paths that do not exist in the concrete system. If this is the case, the

counterexample that is not realizable in the concrete system is identiﬁed as being spurious. To eliminate

a spurious counterexample it is necessary to reﬁne the abstraction. This reﬁnement procedure may be

guided by the returned counterexample and thus performed automatically. This procedure is now known as

counterexample-guided abstraction reﬁnement (CEGAR) [32].

3 A feature-based Classiﬁcation of Veriﬁcation Approaches

We propose a feature-based view to make different veriﬁcation approaches comparable. We classify veriﬁca-

tion approaches by (a) the pursued veriﬁcation goal that captures the intention of the veriﬁcation; (b) the

domain representation that deﬁnes the expected input format of the veriﬁcation approach; (c) the veriﬁca-

tion representation that the underlying veriﬁcation engine uses to perform the actual veriﬁcation; (d) the

speciﬁcation language used to describe the relevant properties that the system should satisfy; (e) and the

veriﬁcation technique that is applied to achieve the veriﬁcation goal. Some aspects of the classiﬁcation

we use have been captured by previously published surveys, all of which focus solely on the veriﬁcation

of model transformations. For example, Amrani et al. [

] propose a tri-dimensional categorization for

model transformation veriﬁcation approaches. They categorize approaches according to (a) the type of the

model transformations that can be veriﬁed, (b) the properties of the transformations that can be analyzed

including termination as well as syntactic and semantic relations, and (c) the employed veriﬁcation technique.

Recently, they presented a generalization of their categorization and introduce a catalog of intents that allows

to classify model transformations according to their intended applications, which includes, but is not limited

to, veriﬁcation [

]. Calegari and Szasz [

] re-use Amrani et al.’s tri-dimensional categorization and suggest

further subcategories for each dimension. Rahim and Whittle [

] classify formal and informal approaches

according to the technique employed to assert the correctness of model transformations. In contrast, we

consider model transformations as one of many possibilities to specify the behavior of a system and, more

generally concentrate on veriﬁcation approaches that assert if a software model adheres to its speciﬁcation.

3.1 Veriﬁcation Goal

The veriﬁcation goal describes the purpose or the intent of the veriﬁcation. We distinguish between three

types of goals: consistency, translation correctness, and behavioral correctness. In the following, we explain

and compare the different veriﬁcation goals. For each goal we provide an example scenario that describes the

veriﬁcation goal in the context of a ﬁctional development process.

剩余42页未读，继续阅读

jtzwy

粉丝: 1
资源: 6

基于特征的软件模型形式化验证技术分类

Deep Learning-Based Classification of Hyperspectral Data

Ranking-Based Classification of Heterogeneous Information Networks

Can under-exploited structure of original-classes help ECOC-based multi-class classification?

Generalization performance of graph-based semi-supervised classification

An-Automatic-Nucleus-Segmentation-and-CNN-Model-based-Classification-Method-of-White-Blood-Cell:WBC核分割，在BCCD，ALL-IDB2，JTSC和CellVision数据集上的定位以及在BCCD数据库上基于CNN模型的分类

python-sphinx-feature-classification-doc-0.3.0-1.el7.noarch.rpm

python-sphinx-feature-classification-doc-0.3.2-1.el7.noarch.rpm

python-sphinx-feature-classification-doc-0.4.1-1.el8.noarch.rpm

python-sphinx-feature-classification-doc-0.4.1-1.el7.noarch.rpm

speech-feature-signal-classification.zip_Speech Feature_语音分类

最新资源