Stochastic Real-Time Systems Modeling与分析博士论文

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

本篇论文《Modeling and Analysis of Stochastic Real-Time Systems》是作者Braham Lotfi Mediouni在2016年完成的一篇博士学位论文，由法国格勒诺布尔阿尔卑斯大学颁发，专攻计算机科学领域。论文的核心内容围绕模型检测与实时计算的理论与方法，特别是在随机实时系统建模与分析方面的深入探讨。论文的研究背景涉及现代信息技术的复杂性和不确定性，尤其是对于那些对时间约束有严格要求的系统，如工业自动化、航空导航或电信网络，其中随机性因素是关键。随机实时系统是指那些系统的行为不仅受控制逻辑的影响，还受到随机事件的干扰，这使得传统的确定性分析方法不再适用。论文的主要贡献可能包括以下几点： 1. **模型构建**：研究者可能讨论了如何构建适用于随机实时系统的数学模型，这可能涉及到概率图模型、马尔科夫决策过程（MDP）或其他形式化的数学工具，以捕捉系统中随机事件的发生和影响。 2. **分析方法**：论文可能会介绍用于分析这些随机实时系统性能的方法，如概率模型检查、统计模型检验或者基于概率的时序逻辑验证技术，以便评估系统是否满足特定的实时性和可靠性要求。 3. **算法与优化**：论文可能还探讨了针对这类系统的算法设计和优化问题，例如如何找到最优策略来处理不确定性，或者如何减少系统的平均响应时间。 4. **实证与应用**：通过具体的实例，作者可能展示了他们的理论如何应用于实际的工程项目，如自动驾驶汽车调度、电力系统调度或者金融交易系统的风险管理。 5. **评审与认可**：论文最后部分列出了评审委员会成员，他们的学术背景反映了该领域的权威性和论文的严谨性，包括来自不同国际知名大学的教授，如Erika Abraham、Enrico Vicario、Eugene Asarin、Kim G. Larsen和Marius-Dorel Bozga，以及指导教授Saddek Bensalem，这体现了论文在全球学术界的专业认可。这篇博士论文为理解、设计和验证复杂的随机实时系统提供了深入的理论框架和技术路径，对推进该领域的研究和实践具有重要的参考价值。

12 Introduction

the environment and the target platform (closed-loop testing), (3) software-in-the-loop

simulation, and (4) hardware-in-the-loop simulation. It increases the quality of the

product by identifying errors at early stages of the design.

Automation: it consists in the development of dedicated tools or scripts to replace manual,

repetitive and error-prone tasks. This includes model transformations, code generation,

test case generation and formal veriﬁcation.

Knowledge capture and management: this concept identiﬁes the model as the central

source of information. It represents all the knowledge about the system, including

functional and extra-functional information.

These concepts are orthogonal to the development methodology, and can be applied to

improve any development process, such as, the V-model, spiral, Scrum or extreme programming

(XP). The most common development methodology in the design of embedded systems is the

V-model. This latter relies on the association of a testing phase to each development step (see

Figure 1.1).

System

Design

Requirements

Analysis

Architecture

Design

Component

Design

Implementation

Component

Test

Integration

Test

System

Test

Acceptance

Test

Figure 1.1: The V-model methodology

The main disadvantage of the V-model is the necessity to develop the entire system at

the beginning which is not a simple task to do when some information about components

or their interactions is not known initially. Model-based design contributes to the V-model

methodology by allowing an early incomplete design of the system at a high-level of abstraction,

and then specifying the missing details as part of a later reﬁnement. It enables, hence, ﬂexibility

regarding changes.

1.1 Designing Complex Systems 13

1.1.2 System Requirements

In a system design project, system speciﬁcation is the main source of information about

the expectations on the system under design. This system is described by a collection of

requirements that represent desired properties of the ﬁnal product. Requirements are extracted

from system speciﬁcation and can be classiﬁed in two categories:

Functional requirements concern the functionality of the system and indicate what the

system should do. These requirements include the expected calculations, data processing

and technical details about the system components.

Extra-functional requirements concern how the system behaves when fulﬁlling its function.

They are described with respect to a (quantitative) metric that permits to judge the

operation of the system. These requirements include performance aspects such as com-

putation time, communication latency, energy consumption, temperature and memory

usage. They also embody sensitive aspects such as security and safety.

Requirements are often expressed in natural language as part of the system speciﬁcation

document. This latter often uses terminologies that are speciﬁc to the client’s business domain,

which sometimes introduce some incomprehension and ambiguity to non-experts in that domain.

In model-based design, requirements are also modeled to facilitate their comprehension and

avoid ambiguity. When formally described using property speciﬁcation languages, they enable

advanced capabilities such as monitor synthesis and automated veriﬁcation.

1.1.3 System Model Characteristics

With the growing complexity of systems, building faithful system models becomes a challenge.

Several factors impact the system complexity, such as the desired functionality and performance,

environmental aspects and the nature of the involved components. As a matter of fact, recent

systems tend to make hardware and software components of diﬀerent nature coexist together.

The designer has to cautiously study the diﬀerent interactions, communications and data ﬂow

to ensure some compatibility in such heterogeneous systems.

The appeal for recent industrial and research activities, such as exploration of outer space,

has created a new era of systems that carry out extremely advanced and elaborate tasks where

time plays a major role. These complex systems have to independently operate in very hostile

and unpredictable environment. To enable an accurate description of such systems, several

key features are required from the modeling languages to manage complexity, describe time

evolution and account for uncertainty.

Decomposition to handle complexity.

A simple yet eﬃcient way to comprehend system

complexity is to model systems as the composition of less complex elements. Following this

divide-and-conquer vision, the design of a system boils down to the design of its components and

14 Introduction

their interactions. Component-based decomposition brings several advantages. The design of

loosely coupled components enables re-usability which signiﬁcantly reduces the design time. It

also opens the doors for the design teams to work in parallel towards common agreed objectives.

Real-time is key.

In complex applications, time has a serious impact on the system state

and inﬂuences its behavior. Timed systems are often deﬁned as systems where not only the

outcome of the operated computation has to be correct, but the time needed to produce it also

matters. In addition to functional constraints, timed systems have to meet temporal constraints.

Considering timing aspects at design time is an obligation as they may impact the correctness

of the system or degrade its performance. The discrete and continuous time frameworks propose

two diﬀerent dynamics in modeling time progression. The former sees time as a succession of

steps whereas the latter deﬁnes it as a continuum. Discrete time has long been considered as a

viable abstraction of the system behavior. However, its modeling capabilities are very limited

when designing time-sensitive systems such as in avionics or in cyber-physical security. In [

the authors emphasize the necessity for modeling time over dense domains by investigating

in-between-ticks attacks on cyber-physical security protocols. This work shows that some

attacks can only be mitigated by models using dense time, as opposed to discrete time.

Probabilities for uncertainty and more.

Probabilistic design puts forward the study of

variability in the system. This variability often comes from the interaction of the system with

external elements in its environment. This environment is, by its nature and size, very hard to

represent and sometimes unpredictable. Abstractions are often required as a means to carry

out very complex processes or interactions. Probabilities allow designers to intuitively represent

uncertainty that may arise from the environment.

Probabilities also enable designers to account for potential imperfections in the software

or hardware that constitute the system. For example, failure rates are the most common

representation of the life cycle of hardware components.

Furthermore, probabilistic behaviors are sometimes artiﬁcially introduced in order to solve

problems due to system symmetry or determinism. For example, the FireWire network protocol

embeds a probabilistic waiting time sampling during the topology leader election in order to

avoid node contention. Another example, in concurrent systems, is the adoption of a randomized

access to shared resources as a mechanism to prevent starvation.

An important aspect of a modeling language is its ability to express complex (real-time and

stochastic) models with a clearly deﬁned semantics. Several modeling formalisms are used

in formal methods and have the advantage to be extensively studied. These formalisms are

endowed with eﬃcient simulation methods and rigorous veriﬁcation techniques. Relying on

such formalisms provides a valuable automation in the design process. This design process

can be even more simpliﬁed and enhanced with automatic code generation, which positively

1.1 Designing Complex Systems 15

impacts the quality of the ﬁnal product since it eliminates potential errors due to traditional

manual coding and repetitive tasks.

1.1.4 Challenges

Model-based design requires a speciﬁc training for the design team in order to acquire modeling

skills and to master the diﬀerent modeling tools. In addition, it may imply training and tools

license costs, and time delays in the design process due to an initial learning curve. Regarding

modeling tools, they often provide a partial coverage of the diﬀerent design steps, as they lack

accurate automatic code generation and/or formal veriﬁcation algorithms.

The main diﬃculty of this approach is the construction of the system model, as it requires

design skills and expertise. This step can be time consuming, especially for complex systems.

Moreover, it consists in chasing contradictory objectives as the construction of a faithful yet

high-level model requires to ﬁnd a good balance between details and abstraction.

The construction of performance models is even more challenging since performance in-

formation are not always available at early design stages. A conventional way to obtain such

information would be to extract it from system speciﬁcation, or to compute it using static

analysis. For example, the performance of a software program can be estimated by its worst

case execution time (WCET). However, considering the impact of the hardware platform and

environment uncertainty adds another dimension to the complexity of characterizing perfor-

mance. As a solution, approaches [

123

] based on the characterization of performance from

concrete system executions have been proposed.

Funconal Model

(BIP)

Code Generaon

Target

Architecture-

Specic Code

Simulaon

Execuon Traces

Distribuon Fi%ng

Performance

Characteriscs

Model Enrichment

Performance

Model

Performance

Analysis

Quantave

Performance

Feedback

Figure 1.2: Overview of the ASTROLABE approach

In ASTROLABE [

123

], illustrated in Figure 1.2, the BIP framework [

] is used for the

construction of system functional models and for the generation of platform-speciﬁc executables.

The collected system executions are analyzed using statistical inference techniques to infer

probability distribution functions describing system performance. Finally, the performance

model is obtained by augmenting the functional model with the inferred performance information.

This workﬂow is meant for general purpose systems and was tested on image processing

algorithms and communication protocols. However, this method embodies several manual

tasks that are tedious and error-prone. More recently, the authors of [

] proposed to use

16 Introduction

property-based testing as a means to generate execution traces, and linear regression for the

extraction of execution time distributions. This method is tailored for the study of web services

response time.

1.2 Analysis of System Models

The quality of a system is dependent of its ability to oﬀer a good performance and its absence

of malfunctions and errors. To mitigate errors, industrials often adopt intensive testing policies,

starting from unit testing, followed by integration testing and ﬁnally system testing. However,

these tests, as intensive and costly as they can be, are unable to cover all the possible usage

scenarios. Besides, the cost of a bug ﬁx grows exponentially with the design stage [

]. The

detection of a bug after the product release is a nightmare for companies since it may imply

prohibitive costs, without mentioning the negative impact on their corporate identity.

Model-based design is supported by a plethora of analysis techniques that allow designers

to identify errors at early design stages, and to extract performance measures that help making

design decisions and avoiding architecture re-engineering costs. Analyzing system models

consists in verifying whether the system satisﬁes formally expressed properties, representing

functional or extra-functional requirements. A system is correct if it satisﬁes all described

requirements. So, the correctness of a system is not absolute, but it is speciﬁc to the considered

speciﬁcation. It is worth mentioning that the accuracy of the analysis results strongly depends

on the ability of the model to faithfully represent the target system.

Formal models are supported by systematic techniques to construct the set of all system

states. This state space serves as a basis for exhaustive exploration through model checking, or

for partial exploration using scenario-based testing or simulation.

1.2.1 Model Checking

Model checking is a veriﬁcation technique that relies on a systematic exploration of the whole

system state space. This technique, illustrated in Figure 1.3, was proposed as the result of two

independent works [

] and [

132

]. Given a system model, a model checker enumerates all the

states of the system and veriﬁes whether the property under veriﬁcation is satisﬁed at each

system state. The exploration can prematurely abort in case the property is violated. The path

leading to the violating state is presented as a diagnostic information, and showcases an error

in the model.

This algorithmic approach for veriﬁcation is faster than deductive methods such as theorem

proving [

]. The challenge with such an approach is to handle large-scale models. With

an explicit state space enumeration, a model checker can handle up to 10

states. More

sophisticated explorations have been proposed in the literature. Symbolic model checking [

114

]

relies on a symbolic representation for state transition systems using Binary Decision Diagrams

剩余235页未读，继续阅读

chennianxiao2012

粉丝: 0
资源: 3

Stochastic Real-Time Systems Modeling与分析博士论文

Introduction to Modeling and Analysis of Stochastic Systems

Stochastic Modeling and Analysis of Telecoms Networks

MARTE/pCCSL: Modeling and Refining Stochastic Behaviors of CPSs with Probabilistic Logical Clocks

Introduction_to_Optimum_Design.pdf

Handbook of Research on Soft Computing and Nature-Inspired Algorithms

Informatics in Control, Automation and Robotics (LNEE 430) 2018

Evaluation of Time Series Forecasting Models: In-depth Analysis of Key Metrics and Testing Methods

4 Applications of Stochastic Analysis in Partial Differential Equations: Handling Uncertainty and ...

Time Series Causal Relationship Analysis: An Expert Guide to Identification and Modeling

[Advanced] MATLAB Stochastic Process Analysis

最新资源