Although the Amalthea meta-model has emerged in the past years to an industrially adopted exchange format for (also safety-critical) embedded software architectures, model checking has been seldom applied to Amalthea models so far. This work presents a simple and extensible translation approach from Amalthea to Promela models for analysis with the widely used Spin model checker. This is a first step towards applying standard state-of-the-art model checkers to Amalthea. 1 This work has been funded by the Federal Ministry of Education and Research (BMBF) as part of PANORAMA (reference no. 01IS18057G). 2 OFFIS - Institute for Information Technology, Oldenburg, Germany, jan.stefen.becker@ofis.de
During many industrial and scientific research projects in the past years, Amalthea [Ec20] has established itself as a modeling standard for multi-core hardware/software (HW/SW) systems. It focuses on timing behavior of these systems and is supported as an exchange format by a growing number of industrial and academic tools. Although not bound to the automotive domain, Amalthea supports many concepts from the AUTOSAR [Na09] and OSEK [OSEK] standards and is therefore primarily targeted to automotive embedded software.
By their nature, many automotive embedded systems are safety-critical (driver assistance systems, for example). Safety standards such as ISO 26262 require a high demand of verification efort during development of those systems. In this paper, a verification approach for Amalthea models is proposed that translates Amalthea models into Promela code for verification with the state-of-the-art model checker Spin [Ho97]. In contrast to classical simulation tools, model checkers such as Spin are able to do a full state space exploration of the input model and therefore proof safety properties (such as task deadlines) formally. Even if a full state space exploration is not possible, experience shows that model checking often finds corner cases that are hard to catch using classical simulation methods. The Spin model checker is state-of-the-art for explicit state model checking of concurrent systems. Its input language, Promela, is a high-level language that allows a high degree of non-determinism. The key elements of Promela are parallel processes that communicate
Copyright © 2021 for this paper by its authors.
Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). via message channels and shared variables. As such, it is dedicated to the verification of concurrent systems.
The goal of this paper is to demonstrate a simple approach for model checking Amalthea models using Spin. The focus in the translation is on simplicity and not on performance (in terms of optimizing the Promela code for model checking with Spin). Key elements of the approach are the following:
It provides a way to model integer time stopwatches in Promela, together with a simple but safe approximation for dense time. This is independent from the Amalthea translation.
The approach can be extended for other scheduling strategies that can be provided as a library.
The translation is template-based, so it can be extended easily to support additional Amalthea elements.
This work is structured as follows. It starts with a short introduction of Amalthea and Promela in Sections 2 and 3. Then, in Section 4, the approach for modeling time is described, with the possibility to stop clocks and with an extension that allows the application of dense time models. The translation of Amalthea to Promela is finally presented in detail in Section 5 and a few experimental results are reported in Section 6. The paper closes with a short summary of related work in Section 7. 2
The Amalthea Meta-Model is an emerging standard for the exchange of multi-core HW/SW architectures between analysis, simulation and design tools. It mainly focuses on timing behavior. It covers many concepts that originate from the AUTOSAR and OSEK standards. Amalthea is divided into a couple of sub-models that target diferent parts of the design. In this work, the following are relevant.
Software model describes the software units (tasks and runnables) of the system including an abstraction of the control flow.
Hardware model defines the layout of the executing hardware environment, with a focus on communication paths.
OS model characterizes the operating system (OS), i. e., the task schedulers, synchronization mechanisms, and timing overheads caused by OS activities such as context switches. In this paper, schedulers and OS Events are used from the OS model.
Stimuli model contains the activation patterns for tasks. This publication considers timetriggered (i. e. periodic) stimuli only.
Mapping model brings all the parts together by describing the allocation from software and data to hardware.
In the context of this work, the most important part is the software model. Its basic elements are so-called tasks and runnables. A tasks is the smallest unit of software that is managed by a scheduler in the OS and assigned to a core for execution. A task is in most cases a sequence of runnables which in turn can be seen as an equivalent of a function. Tasks and runnables are modeled as so-called activity graphs in Amalthea, whereby a single item in this graph is an abstraction of low level processor instructions, such as memory access, computations, or synchronization primitives. The relevant parts of the software model are described in more detail during the translation in Section 5. A complete documentation of Amalthea can be found online3. 3
This section gives a short overview of the Promela syntax and semantics used in this paper. For a more comprehensive definition the reader is referred to the Spin manual [Ho04] or the extensive online documentation4.
The primary elements of Promela are processes. A process is declared using the keyword proctype. Active processes (marked with the keyword active) are instantiated automatically, other processes must be instantiated explicitly from within other processes. The process body is a sequence (or, more precisely, a graph) of statements separated by ; or ->5. The syntax is a mixture of C and Dijkstra’s guarded commands. A statement is enabled if it can be executed in the current state, otherwise it blocks. In Promela, Boolean expressions are statements that do not have a side-efect and are enabled whenever they evaluate to true. Branching is possible using if and do blocks. A do block is repeated until a break statement is reached. A branch in an if or do block is enabled whenever its first statement, called its guard is enabled. If more than one branch is enabled, one is selected non-deterministically; if none is enabled, the whole block blocks.
Normally, in each step one non-blocked process is selected non-deterministically to execute one statement. A sequence of statements can be made atomic by surrounding them with an atomic block. However, atomicity is lost, i. e., another process can gain control, when a statement blocks, and resumed when the blocking statement becomes enabled (which does 3 https://www.eclipse.org/app4mc/help/app4mc-1.0.0/index.html 4 http://spinroot.com/spin/Man/promela.html 5 As a convention, -> is used after the first statement in an if or do branch. Beware that the -> is overloaded in Promela and also used as part of an inline if-then-else. not mean that the process gains control immediately). An atomic block is enabled whenever its first statement, the guard, is enabled.
Processes communicate via shared variables and message channels. In this work, only a special type of channel is used, so-called rendezvous channels. In a rendezvous, a message is passed between two processes if the send and receive statements are executed at the same time. Otherwise, send and receive statements block until the rendezvous can be executed. The advantage of rendezvous channels via bufered communication is that no message queue needs to be stored in the state vector, so they are very cheap during verification. Messages are sent using the ! and received using the ? operator. A message consists of multiple fields separated by commas on the right-hand side of the operator. By convention, the first field contains the message type, and the remaining fields message parameters.
Special statements used in this work are the skip statement that exists for syntactic reasons and does nothing, the else statement that is only valid as a guard in an if or do branch and enabled when no other branch is enabled, and the timeout statement that is enabled only if no other process can execute. 4
By design, Promela does not have a notion of time. In the following, it is described how time progress can be explicitly modeled, though. Although many approaches for modeling clocks in Promela have been proposed [BD98; MMJ11; TC96; Tr07], none ifts all the needs of this paper: Because we need to model preemptive processes with non-deterministic execution times, we need a wait function that suspends the calling proces for a non-deterministic amount of time drawn from some interval »CMIN CMAX¼. Furthermore, time is only accounted when an enablement condition COND evaluates to true. The main idea is to use a global time increment variable delta and Promela’s timeout statement. Processes that want to wait for an amount of time, communicate the minimum time delay until their next action to a timing supervisor process. This process uses the timeout statement to initiate and coordinate a time increment whenever no other (untimed) progress is possible in the system. Listings 1 and 2 show the Promela code for the waiting process and the timing supervisor. Their interaction is visualized in Figure 1. The clk variable ist used to track elapsed time. The Boolean step variable in lines 6 and 9 of Listing 1 works as a synchronization barrier. Initially, step is 1. The expression step == 0 cannot be passed unless the timing supervisor process initiates a time step by setting step to 0. When this happens, all the processes that are in a waiting state start executing again and adjust delta_min and delta_max in order to agree on the minimal and maximal delay until the next action. Afterwards, the supervisor process selects a time increment delta and resets step to 1, which starts a new discrete step. In the proposed implementation, one of fmin min ¸ 1 maxg is selected (provided min max), which allows reaching all possible time increments as well as to “shortcut” larger ones in order to find safety violations earlier.
Waiting processes stay in a loop for multiple time steps, whereby they participate in the election process and increment their clock only if the COND constraint evaluates to true. This allows later on in Section 5 to disable time progress for preempted tasks. 1 inline wait(CMIN, CMAX, COND) { 2 atomic { 3 clk = 0; 4 do 5 :: clk >= CMIN -> COND; break 6 :: clk < CMAX -> COND && step == 0; 7 delta_min = MIN(delta_min, MAX(CMIN - clk,1); 8 delta_max = MIN(delta_max, CMAX - clk); 9 step == 1; clk = clk + delta 10 od 11 } 12 }
List. 1: Waiting for an amount »CMIN CMAX¼ of time. 1 do 2 :: timeout -> d_step { 3 delta_min = MAX_TIME; delta_max = MAX_TIME; 4 step = 0 }; 5 timeout; 6 atomic { 7 if 8 :: true -> delta = delta_min 9 :: delta_min < delta_max -> delta = delta_max 10 :: delta_min < delta_max -> delta = delta_min + 1 11 fi ; send_event(TIME_STEP,delta); step = 1; 12 } 13 od
It has been shown by [Fe07] that many problems, including safety properties such as satisfaction of deadlines, are undecidable for preemptive scheduling in dense time. As a consequence, there is no exact encoding technique for dense time clocks that guarantees a ifnite state space. Hence, classical abstraction techniques such as region automata [AD94] or diference bound matrices (DBMs) that are exact for timed automata, can be adopted to preemptive scheduling only in some special cases [Fe07] (e. g. deterministic response times that usually do not apply to Amalthea) or for the price of (theoretically unbounded) over-approximations [CL00]. The approach in this work is to provide a simple but safe integer-time over-approximation for the dense time clock values. Because clock values are only compared to integer constants, it is suficient to store the integer part of the clock values in the state space, provided that for any reachable state ¹ º with real-valued clock vector R, the state ¹ bcº is reachable in the discretized approximation. The approximation is based on the following observation: Assume that in some dense time run, a clock all tasks all tasks .. : Task
:Timing Supervisor timeout step := 0 timeout step := 1
choose is resumed in some step and runs until being stopped in some step ¡ . Let’s denote the values of in steps and by 2 R 0, and the time stamps of these steps by 2 R 0. It holds = which implies b c = b c ¸ b c b c ¸ with 2 f 1 0 1g (1) In a dense time interpretation of the Promela model, delta = b 0c bc contains the diference between the integer parts of the current and last time points, and the clk variable tracks the integer part of a dense time clock. Listing 3 extends the wait function from Listing 1 and adds adjustments to clk for the diferent possibilities for the error . This is done by tracking (in the suspended variable) whether the clock was suspended during the last time step, and, in that case, allow alternative time increments clk := clk ¸ 1. 5
In this section, the translation of an Amalthea model into Promela is described. Additionally to the timing supervisor which is part of the initial Promela process, a Model Checking Amalthea with Spin 7
List. 3: Waiting for an amount »CMIN CMAX¼ of time, with dense time adjustment process is created for each task, each scheduler, each time-triggered stimulus, and each timing constraint. These processes communicate via rendezvous channels. Amalthea elements that store state information are encoded as global variables. The Promela encoding uses global variables for mode labels, OS events, task states, and activation counters.
Mode labels are used in so-called mode switches to model operation-mode dependent control flow and mode changes. Mode labels can be shared by multiple tasks. For each mode label , the translation introduces a global variable var.
OS events are synchronization primitives belonging to the operating system. OS events are global Boolean variables and are encoded in Promela as such. However, the handling is special: The owner task of an event can wait for one or a set of events to be set. In Amalthea, this may either be passive waiting, i. e., the task switches to waiting state and gets activated once the event is set, or active waiting meaning the task stays in running state while waiting. Other tasks may set an OS event to inform the owner about some event, e. g., some data now being ready for processing. Task execution states are stored in a global array named states. We assign to every task some index in this array. The advantage of an array over one state variable per task is that scheduler implementations in Promela can be easily reused: The task
IDs (i. e. indices in the state array) are sent to a scheduler via its comm channel with an activation request. So there is no need to hardcode execution state variables in the scheduler implementation.
The prototype implements the extended OSEK task state automaton [OSEK] shown in Figure 3. The original state automaton defined by Amalthea is an extension of it that introduces variants of the running and preempted states that are entered when the task is actively waiting, or preempted during active waiting, respectively. These task states are purely conceptional, however, so it is possible to use the simpler OSEK task automaton without changing analysis results. The currently executing task is in the running state, and tasks that are ready for execution are in the ready state. Initially, and after termination (until the next activation), tasks are in the suspended state. In the Promela translation proposed in this work, the task process can send activate, wait, release, and terminate messages to the scheduler process, which acknowledges them by changing the task state accordingly. At the same time, the scheduler can start or preempt other tasks, according to the scheduling strategy. In a fixed-priority preemptive scheduling, for example, it will always put the highest priority task to running.
SUSPENDED preemt
WAITING activate terminate start
READY RUNNING resume wait Listing 4 shows the Promela code frame for tasks. The variable trigg counts pending activations for task . For tasks with a periodic stimulus, for example, this counter is incremented by a stimulus process as shown in Listing 5. The task frame is an infinite loop. At start of the loop, the process waits for some pending activation. When there is a pending activation, the task process sends a message with an activation request, its ID and scheduling parameters (the task priority in this case) to its scheduler , via the channel comm. Then, the instructions (activity graph items in Amalthea) of the task are processed. Every item in the instructions sequence is an atomic block that is guarded by the condition states[ ]==RUNNING, so they are only processed when the task has been put into running state by the scheduler. At the end of the loop, a termination signal is sent to the scheduler. In the following, the translations of individual activity graph items are described. First of all, calls to other Runnables are inlined during translation.
Ticks are the primary element in Amalthea to model execution time. Ticks are an abstraction of some arbitrary instruction sequence that is characterized by an lower () and upper () execution time bound. Ticks are translated as wait(, , states[ ]==RUNNING). Here we see the need for the COND parameter in the wait function: Time is only consumed when the task is in running state. 1 active proctype task () { 2 do 543 :: /a*tocimonimscmt{r!tuArcCitTgiIgoVnAsTE>s,e0qu-e>n,cteri*g/}g; --; 654 6 atomic {states[ ] == RUNNING; 78 7 comm!TERMINATE, ,0 } 8 od 9 }
List. 4: Task process frame
Model Checking Amalthea with Spin 9 9 10 } 1 active proctype stimSt() { 2 int clk, t_next; 3 atomic { t_next = ; do :: wait(t_next, t_next, true) ; t_next = ; /* for each stimulated task : */ trigg = trigg + 1 od }
stimulus St with recurrence (i. e. period) and ofset .
Switches are used to model control flow. In Amalthea, there are two types of switches: In a mode switche each branch is guarded by a Boolean condition over the current values of mode labels. In a probability switch each branch is taken with some fixed probability, independent from the system state. A switch is encoded as an if block if :: states[ ]==RUNNING && 1 -> /* instructions of branch 1 */ :: states[ ]==RUNNING && 2 -> /* instructions of branch 2 */ /* ... */ :: states[ ]==RUNNING && -> /* instructions of branch */ fi For mode switches, is the enabling condition for the th branch, conjunct with :1 ^ ^ : 1 to make the branches prioritized. For probability switches, any branch is possible, so set 1 := := := true.
Label access is not part of the Promela code in general, except for write access to mode labels, which is translated as atomic { states[ ]==RUNNING; var = }, where is the label written, and the new value (Amalthea uses symbolic constants to represent values, which are mapped to integers during the translation). Other label access is not translated, because Amalthea does not model data values and therefore it does not afect the state space. Of course it is possible to consider the communication overhead in the translation, though, by inserting appropriate wait statements at the point of label access. Possible approaches for calculating safe bounds on the communication overhead are presented in [Hö19; Kr19]. Simulating communication overhead (e. g. in form of bus transactions) is outside of the scope of this publication.
OS events are handled as follows: Setting and re-setting OS events is translated the same as mode label write access above, where the Boolean variable var for event is set to true in case of setting events, and to false in case of a reset. Active waiting for some event , i. e., the task is continuously running while waiting, can be translated very easily to states[ ]==RUNNING && var. Because in Promela conditions block a process until they evaluate to true, this statements causes the task process to wait for the event. Passive waiting is a bit more complex: For safety properties, such as event chains and worst-case response times, special processes are generated that act as observers. These cannot be implemented outside the simulation model (as so-called never claims) as usual in Promela, because otherwise it is not possible in Promela to use helper variables for tracking elapsed time. So the observers are regular active processes. For sending events to the observers, a macro send_event(evt, data) is generated that logs6 the event and sends it via rendezvouz channels to the observers. The observers handle events in an atomic sequence and acknowledge them via another rendezvouz channel. This passes control back to the process that sends the event without the possibility of being interrupted by other processes. A special message TIME_STEP is used by the timing supervisor to inform the observers about time increments.
For reason of space, it is not possible to show scheduler and observer implementations here. The interested reader can find examples in the source code available online (see next section). 6
In order to evaluate the approach, the translation has been applied to three example
Amalthea models: The democar and state machine examples shipped with the APP4MC
platform, and t
Spin is able to do a full state-space exploration of the state machine example. It has 1158 states and 1842 transitions.
In the democar example, Spin finds the deadline violation for Task_10ms. Without observers, a full state space exploration results in about 27 106 states and 65 106 transitions.
Because a Promela implementation of the time-slice scheduling used in the FMTV challenge for the GPU tasks is future work, a fixed priority preemptive scheduling 6 The prototype implementation inserts printf statements into the code that are emitted by Spin when replaying a counterexample trail. The output can be used to produce an execution trace of the Amalthea model. 7 https://gitlab.com/jansbecker/ase2021
has been used also for the SFM and Localization tasks in the model. When assigning the same priority to both tasks, a deadline violation for the SFM task is found after 15681 steps (using depth-first search).
Within the experiments, no false-positive deadline violations due to the over-approximation of dense time have been reported. So it seems that the price of over-approximation is low. 7
In this work, a translation from Amalthea to Promela is presented that allows verification of safety properties of Amalthea software models using the Spin model checker. The translation is surprisingly straight forward after making a few building blocks, such as stoppable clocks, available in Promela.
Most verification tools for Amalthea use simulation and static analysis approaches. The most famous industrial tools of this kind are probably the TA Tool Suite8 by VECTOR and the INCHRON Tool Suite9. Besides these, a number of verification techniques have been applied to Amalthea models in the context of case studies, e. g., [Co16; Hö19; Kr19]. Among those, [St16] is the only one known to the author that applies explicit state model checking to Amalthea. Compared to the Promela translation presented here, the model checker used in that work, RTAna2, is specialized to the analysis of task networks. Timing extensions to the Spin model checker, respectively approaches to model time in Promela, have been published already some years ago. The best known ones are probably [BD98; TC96], some more recent ones can be found in [MMJ11; Tr07]. Among these, only [Tr07] handles stopwatches, which is essential for modeling preemptive scheduling. Compared to the cited work, the approach developed here is less simplistic due to the combination of clock suspension, variable step sizes and a dense time adjustment. Nevertheless, it is worth seeking for a more eficient implementation that needs fewer process interactions per time step. Also, further research investigates into other approximations for dense time that hopefully guarantee bounded errors. [AD94] [BD98]
Alur, R.; Dill, D. L.: A theory of timed automata. Theoretical computer science 126/2, pp. 183–235, 1994.
Bošnački, D.; Dams, D.: Integrating real time into Spin: A prototype implementation. In: Formal Description Techniques and Protocol Specification, Testing and Verification. Springer, pp. 423–438, 1998. 8 https://www.vector.com/de/de/produkte/produkte-a-z/software/ta-tool-suite/ 9 https://www.inchron.com/tool-suite/ [CL00] [Co16] [Ec20] [Fe07] [Ho04] [Hö19] [Ho97] [Kr19] [MMJ11] [Na09] [OSEK] [St16] [TC96] [Tr07]