• Ingen resultater fundet

# MoVES - A tool for Modelling and Veriﬁcation of Embedded Systems

N/A
N/A
Info

Hent

Protected

Academic year: 2023

Del "MoVES - A tool for Modelling and Veriﬁcation of Embedded Systems"

Copied!
209
0
0
Vis mere ( Sider)

Hele teksten

(1)

(2)

(3)

(4)
(5)

(6)
(7)

1

2

(8)
(9)

(10)
(11)

(12)

(13)

(14)

(15)

(16)

(17)

(18)

(19)

(20)

1

(21)

(22)
(23)

## MPSoC model

(24)

(25)

1

(26)

(27)

(28)

### So far only periodic tasks have been discussed. In order to give a more realistic model, we want to model non-periodic tasks too. Non-periodic tasks can model events that occur in a non predictable way, or events that occur without a fixed period. Examples of such are user input of a system. In a mobile phone this could be the activation of buttons by the user, which are pressed at random times. According to [11] there are two types of non-periodic tasks. The sporadic tasks which have a hard deadline and the aperiodic tasks which have a soft deadline. Using the three types of deadlines, described in the previous section, it is possible to model non-periodic tasks with firm deadline. If a firm deadline is missed the system will continue and the execution of the task will stop, since there is no point in continuing (Recall that, a task with firm deadline adds no value to the system after its deadline).

IdleWait Idle

//Wait for next period x<=ptime

i:int[emin,emax]

!finishSignalsPending() ready!

initNextPeriod(i) trigger?

initTask() i:int[emin,emax]

x==ptime &&

readyForNextPeriod() ready!

initNextPeriod(i)

(29)

(30)

(31)

(32)

(33)

(34)

2

(35)

3

(36)

(37)

(38)

(39)

(40)

i

i

(41)

## Timed-Automata Semantics

(42)

(43)

1

(44)

### combinations of guards and invariants that are used to make the task change

(45)

Offset

//Wait for offset x<=offset-1

Start

ReadyDynamic

x<=1

Running3 x<=1

Running2 x<1 IdleWait

//Waiting for next period x<ptime

Running Ready Idle

//Waiting for next period x<=ptime

//Finished waiting for offset x==offset-1 setPeriodClock() taskHasOffset()

initOffset()

!taskHasOffset() initNoOffset()

deadlineNotMissedYetOrSOFT() setWaitForUpdateDynamicScheduling() //Time unit completion

x==1

updateDynamicScheduling()

//Complete one run x==1 runOneTimeUnit()

//Continue run x>0

ensureRunCompletion() readyForNextRun() initOneRun() taskFinishAtPeriodEnd() ||

FirmdeadlineMissedAtPeriod() finish!

finishAtPeriodEnd() x>ptime-1

setPend()

taskFinishBeforePeriodEnd() ||

FirmdeadlineMissedBeforePeriod() finish!

finishBeforePeriodEnd()

taskHasMoreRuntime() preempt?

setPreempted() deadlineNotMissedOrSOFT()

run?

i:int[emin,emax]

x==ptime &&

readyForNextPeriod() ready!

initNextPeriod(i)

(46)

### their period, and move to the Idle state if they finish at the end of their period.

(47)

Offset

//Wait for offset x<=offset-1

Start

ReadyDynamic

x<=1

Running3 x<=1

Running2 x<1

MissedDeadline

IdleWait //Waiting for next period x<ptime

Running Ready Idle

//Waiting for next period x<=ptime

deadlineMissedRun() updateMissedDeadline() FirmdeadlineWillMiss()

firmDeadlineMisses()

//Finished waiting for offset x==offset-1 setPeriodClock() taskHasOffset()

initOffset()

!taskHasOffset() initNoOffset()

deadlineNotMissedYetOrSOFT() setWaitForUpdateDynamicScheduling() //Time unit completion

x==1

updateDynamicScheduling()

//Complete one run x==1 runOneTimeUnit()

//Continue run x>0

ensureRunCompletion() readyForNextRun() initOneRun()

deadlineMissed() updateMissedDeadline()

taskFinishAtPeriodEnd() ||

FirmdeadlineMissedAtPeriod() finish!

finishAtPeriodEnd() x>ptime-1

setPend()

taskFinishBeforePeriodEnd() ||

FirmdeadlineMissedBeforePeriod() finish!

finishBeforePeriodEnd()

taskHasMoreRuntime() preempt?

setPreempted() deadlineNotMissedOrSOFT()

run?

i:int[emin,emax]

x==ptime &&

readyForNextPeriod() ready!

initNextPeriod(i)

### Figure 3.3: The task template including deadline miss

Referencer

RELATEREDE DOKUMENTER

Occupational Science and Occupational Therapy, User Perspectives and Community-based Interventions, Department of Public Health, University of Southern Denmark, Odense,

Using a complex modelling approach, we have presented sufficient conditions – expressed by properties of the system matrices – for asymptotical stability of a class of dynamical

This property can be used to prove geometrically, that every dipath in X is dihomotopic to a dipath on the edges of I n – modelling a serial execution. Conclusion Every execution

A group in Paris, France [34] , developed an approach to the high level synthesis of embedded systems based on the description of the system in VHDL [35] , and the translation of

During the construction of line B, line A may be operating and the risk assessment considered potential damage to the line A from dropped pipe joints during

Nord Stream 2 AG shall therefore operate the pipelines according to a management system for Pipeline Integrity Management and maintain an operating organisation which at all

Based on the modelling results the intensity of the impact from a major oil spill is assessed to be medium with a transboundary extent and a medium duration.. Overall, the impact

Spread-Spectrum is a means of information transmission in which the modulated signal occupies a bandwidth in excess of the minimum necessary to send the information; the signal

discussed in Probst and Hansen [2008]) will be used to calculate a superset of attacks that can be caused by an attacker at a given location in the specified system. Thus the tool

The studies in this work are based on a unique dataset, which comprises field measurements from numerous fuel cell based backup power systems, which have been operating

System” which refers to the embedded Linux System that you wish to build on a Xilinx

The development moves from modelling challenges at the level of an individual wood component and its fibre distribution (a), to a method of modelling and representing fibre

platforms, including embedded processors (Microblaze and PowerPC) running different operating systems (Xilinx Kernel, Linux and without OS). Separation of the model from the

The authors attempted to indicate potential directions of modernization of currently operating energy systems on the example of a heating company operating in Poland (combined

the comunication issue at respectively service layer and network layer, since the purpose of the type system is to ensure that a message with the wrong type is never send nor

Embedded systems kernel development and implementation, single address space operating systems, generalized bootstrapping.... 2.2 Introduction to

The simplest way of formalising the Nelson and Winter theory of the firm in a way which opens up for a subsequent specialisation of firms is to consider the overall task of

Based on a sample of 197 public-to-private, 240 divisional and 349 private-to-private (which of 72 are European) RLBOs from 1980-2015, the post-IPO operating and stock performance is

Since operating systems generally exist as software executing on a processor, it would be possible to model the execution time requirements of operating system functions as

Accessing a memory cost power and the goal of this thesis is to design a software model, which from a address and data trace from the system, can calculate the memory systems power

Another possibility is that the sending station may be allowed to send all waiting messages each time it receives the token (so-called exhaustive service), or that it can send for

The main task of this project is to take a model of a system created with the SE2 CASE tool and to generate Java code, which implements the system created by the CASE tool

Thus, there is a need for a mapping tool which performs theAn important design task that has to be supported by such tools is the mapping of the automotive electronic

Vælg dit sprog

Hjemmesiden vil blive oversat til det sprog, du vælger.

Foreslåede sprog til dig:

Andet: