Afgeronde rechthoek: Top of book Afgeronde rechthoek: Managers track Afgeronde rechthoek: Technical track Afgeronde rechthoek: Previous page Afgeronde rechthoek: Home




Page contents

Formal specifications. 2

Fundamentals. 2

Higher-level descriptors. 2

Advantages and limitations of mutual independence. 2

Formal software specifications. 3

Systems. 3

Digital systems. 3

State. 3

Deterministic systems. 3

Tasks. 3

Operands. 3

Occurrence. 3

Task Scheduler 3

Threads of Execution. 4

Thread Switcher 4

Task descriptor 4

Invoking the Task Scheduler 4

Course and Fine Grain Scheduling. 4

Task Interference. 4

Task Characteristics. 4

Real-time Systems. 4

Scheduling algorithms. 4

Fault tolerance. 4

Triggers. 4

Programs. 5

Program Blocks. 5

Low-level and High-level Programs. 5

Concurrent access. 5

Exchange of information between threads. 5

Communication. 5

Methods. 5

Summary. 5

Tasks and methods. 5


Formal specifications


A view of a subject is a consistent set of observations that are made in relation with one or more usages of the subject. With respect to these usages, the view completely describes the subject. A subject may be described in several different views. These views may be interdependent.

A formal specification of a subject provides a clear and complete description of all relevant aspects of a given view of that subject. Thus, a single formal specification does not necessarily describe all aspects of the corresponding subject. It only describes all aspects that are relevant for the usage that underlies the corresponding view.

Ideally, the formal specification uses atomic description elements that are mutually independent and that together constitute a complete view of the subject. Apart from these atomic description elements, the specification may contain description elements that will be used to handle the subject or the description of the subject. Any formal specification must make a clear distinction between the set of atomic mutually independent descriptors and secondary descriptors that are configured from or derived from the atomic descriptors. As much as is possible, a formal specification must try to avoid the usage of description elements that are derivatives of the set of mutually independent basic description elements.

Higher-level descriptors

Independent descriptors may be grouped and such a group may be treated as a higher-level descriptor. Higher-level descriptors are not derived from independent descriptors. Since higher-level descriptors are independent of the descriptors that are not part of it, it is possible to create hierarchies of higher-level descriptors that contain higher-level descriptors or atomic descriptors. A higher-level descriptor can be described in detail by describing its constituents. The relation between the high-level descriptors and its constituent descriptors must be known to the audience.

Advantages and limitations of mutual independence

If a formal specification uses a set of mutually independent descriptors, then the check whether the description is complete and consistent becomes simple.

The change of one of the mutually independent descriptors does not affect any of the other independent descriptors. It might affect existing derived descriptors. If the effect of change of specification must be minimized, then the formal specification must not contain any derived descriptors, or the dependence of the derived descriptors on the atomic descriptors must be clearly specified.

If some atomic descriptors are missing, or are replaced by non-specified high-level descriptors, then there will be situations that cannot be described correctly with this set of descriptors. Similarly, if the specification of an implementation is limited to a restricted set of high-level design elements, then there will be situations that the target product cannot be implemented in a natural and efficient way.

Formal software specifications

Due to the characteristics of modeling tools and programming languages, software specifications always make use of derived and higher-level descriptors. Current programming languages prohibit that software systems are specified in a set of mutually independent atomic descriptors. This deficiency becomes apparent when in a real-time system interrupts break up the normal execution of a program.

Formal software specification documents do not normally include the specification of the dependence of high-level descriptors on atomic descriptors. This report provides such a specification.


A system is a subject that has a dynamic relation with its environment. A fundamental characteristic of all subjects that have a dynamic relation with their environment is the fact that their descriptors can be divided in two sets. One of these sets contains the actions of the subject and the other set contains the assets of the subject. The values of the assets together define the ‘appearance’ of the subject. The actions define its behavior. The change of the value of an asset may be a continuous function of time or the value may change in discrete steps.

Digital systems

This document will only consider digital systems. For digital systems, the values of assets change in discrete steps. However, the environment of these systems may change in a continuous manner.

Digital systems cannot themselves cause continuous state changes. However, in cooperation with their environment, such as digital to analog peripheral equipment, digital systems can cause a continuous response. Similarly, digital systems cannot directly react on continuous changes of their environment. However, digital systems can react on digitized analog signals.


The collection of values of the assets of a digital system determines the state of that system. The execution of an action may alter the value of one or more of the assets. Thus in principle the actions and the assets are interdependent. However, in a given state of the observed system, the values of the assets are fixed. Thus, in a given state, the actions and the assets are independent. States can be divided in sub-states. The asset values in a sub-state are a subset of asset values of the state. A single asset value forms the smallest sub-state. Such a sub-state is called an atomic sub-state. In a system that acts in discrete steps, actions can be interpreted as a sequence of state-transitions. State-transitions are caused by internal or external triggers. A trigger can be the result of a change of conditions or it is the result of a change of a target. For example, in resource-restricted conditions, a trigger can be caused by the fact that the subject has no longer access to a required resource. A trigger starts an operation. An operation is a sequence of indivisible operation steps, each of which causes a state transition. An indivisible operation step is executed by an operand. Partly, the operation is determined by a planned program. The environment and the initial state also influence the operation. An action is the impression of behavior that results from the execution of the underlying operation.

Deterministic systems

A completely specified system is deterministic. However, the environment of a system is usually only known in stochastic sense. If the system is influenced by its environment, then the future of the system is not fully determined. It may be determined stochastically. If at a given instant the interference of the environment with a deterministic system is exactly known, then the reaction of a deterministic system is also fully determined.


Within certain limits, the future of a well-defined system is fully determined. This is achieved by specifying a set of tasks and a set of task scheduling criteria. A task is a set of operations that must be accomplished to achieve a certain target. The objective is to reach a state that is a member of a collection of states that all suffice the target. Often, such a collection is characterized by a common sub-state.


The tiniest action corresponds to an indivisible operation. It is performed by an operand. In a digital system, an operand is executed by a processing unit. An operand maps a set of asset values into another set of asset values. The indivisible operation is fired by a trigger. If at a single instant, two or more independent tasks perform each an indivisible operation, then this causes a single state-transition.


The combination of all indivisible operations that occur at the same instance is an occurrence. Tasks that belong to items outside the scope of the current subject are considered to belong to the environment. Each state-transition is caused by an occurrence. An occurrence consists of actions inside the scope of the considered subject and actions that are part of its environment. The state transitions that take place inside the scope of the subject together form the controlled part of the occurrence.

Task Scheduler

Many systems feature a set of concurrent tasks that run in parallel. Apart from the initial main task, each of these tasks is started by a task scheduler. A task scheduler is part of just another task. Several task schedulers may exist that work in parallel. Usually, a task scheduler exists for each processing unit. However, it is possible that a single task scheduler serves multiple processing units.

Threads of Execution

In case of multiple concurrent tasks, part of the main task constitutes a task scheduler. Tasks can indirectly initiate other tasks. If that task is not executed in concurrence with the original task, it is not considered as a new task. Instead, it is considered as a sub-task of the original task. New tasks are always started by a task scheduler. The new task may execute on another thread of execution. The threads that run on different processing units work concurrently. However, at every instant, only one thread can be active on the same processing unit. A thread of execution is not the same thing as a task. A sequence of tasks may reside on a single thread.

Thread Switcher

A thread is managed by a thread switcher. The tread switcher divides the processor time between the existing threads. A thread inherits its priority from the task that currently runs on that thread. The task scheduler and the thread switcher work in close cooperation. The task scheduler may request the thread switcher to add, delete, pause or reactivate a thread. Often the thread switcher and the task scheduler are combined in a task manager.

Task descriptor

A task is a fundamental descriptor. A thread is only an implementation facet. However, the way that tasks are distributed over threads is again a fundamental design aspect. It may deeply influence the behavior of the resulting system.

Invoking the Task Scheduler

If the task does not itself implement a task scheduler, then the initiation of the new task is done by invoking an existing task scheduler. In multitasking systems, task scheduling may be delegated to a centralized task-manager. At its start, the task has a priority. This priority is used by the task scheduler to decide which action must prevail when two or more tasks want to use the same resource. The lifetime of a non-cyclic task ends when it has achieved its final target. The task scheduler determines the initial priority of a task. During its lifetime, the priority of the task may change upwards or downwards. Usually the task itself determines the new priority setting. However, it may be advised or convinced to do so by another system component. At each moment, only one action is active in each task. Actions can trigger other actions. Usually, these new actions belong to the same task.

Course and Fine Grain Scheduling

The task scheduler performs course grain scheduling. A scheduling program describes the scheduling plan. The task itself may perform fine grain scheduling. The activity within a task is described by a task program. The fine grain scheduling is done by following different execution paths depending on the values of the assets that exist in its current domain. The domain of a task is part of the scope of the considered subject and in addition, it covers part of the environment of the subject. Thus, the path selectors inside the task program use asset values that are taken from the current domain. The domain of a task is determined by the capabilities of its implementation. A given implementation can be designated limited access to the implementations of the assets that exist in the environment that is crossed by the task. The assets that are accessible by the current action determine the current domain of the task. An execution path corresponds to a trajectory through the set of connected state transitions. Each step in this trajectory corresponds to the start of a new subtask. A subtask is not the same thing as a task. Subtasks are not scheduled by a task scheduler.

Task Interference

During the completion of an action that is part of a given task, a concurrent task may change asset values in the domain of the first task. Consequently, the first task may decide to take a different execution path than it would have done without the interference with other tasks. The interference between concurrent tasks may take place in the middle of the execution of an action that is described by a high-level description element. In that case, the description element gives an improper view of the actual situation.

Task Characteristics

A task may be periodic or it is sporadic. Sporadic does not say that the task is non-cyclic. If the sporadic task is cyclic, it does not have a fixed period. In a periodic task, the target must be reached at each cycle and within the period. A task may have a deadline. The deadline of a periodic task is set by its period. A task has a hard deadline when the system or its environment will get in disorder when the deadline of the task is not reached. A task with a hard deadline is a real-time task.

Real-time Systems

A system that implements a real-time task is a real-time system. In a real-time system, one of the task schedulers determines when a given real-time task must start. In order to perform its task, the real-time scheduler uses its knowledge about the execution time of the task. Due to interference with other tasks, the execution time is often only known in statistical sense. For hard deadlines, the scheduler must use the worst-case execution time. For soft deadlines, it may use the expected execution time. A task with a soft deadline may change its priority.

Scheduling algorithms

The priority of a task with a hard deadline is completely controlled by the task scheduler. However, during the run of a task a new priority may be proposed to the task scheduler. The scheduler may then decide to reschedule the tasks. In order to determine the start times and the priorities of the tasks that posses a soft or hard deadline, the scheduler uses a scheduling algorithm. By controlling the priorities of real-time tasks, the scheduler influences the speed of execution of that task.

Fault tolerance

A soft deadline primary task and a hard deadline repair task may be paired, such that the pair always meets the hard deadline. After surpassing the soft deadline, the task scheduler will stop the primary task. The resulting time will then be used for the repair action. The paired tasks implement a fault tolerant solution.


A trigger is a complex concept. It represents the conclusion taken from a comparison of the current state or sub-state with a target state or sub-state. Not the conditions or the reasoning, but the conclusion is relevant for the trigger. In detail, a trigger consists of a sub-state that represents a set of existing values of assets, a set containing one or more target states and a collection of possible tasks or actions that must be started to come from the current sub-state to one of the target states. The assets that are evaluated are a subset of the domain of the current task. This domain may be larger than the system part that is crossed by the current task. Partly or completely, the trigger may be determined by a program. The program can be a scheduling program or an intra-task program.


A program is an action plan and implements one or more algorithms. A program contains a tree or network of operators and path selectors. Operators and path selectors are described by program statements. The trigger of an operator in a program corresponds to the program statement that specifies this operator. A statement that describes an operator may also be interpreted as the trigger of that operator. Based on a Boolean expression the path selector decides what path must be selected. The Boolean expression is a function of asset values. Higher-level constructs may implement more complex path selectors. Examples are loop control statements and multi-path switches. Simple Boolean path selectors that act on a single Boolean asset value are called atomic path selectors. The atomic path selectors are implemented by the processing units. With the help of the path selectors, the program plans a set of possible trajectories through the forest of possible states that the considered subject must take according to the current task. The actual trajectory is influenced by the environment and by other tasks that pass through the domain of the task. The planned trajectory may be interrupted. An intervening schedule may decide to stop the task and end therewith executing the task’s program.

Together with the environment, with the running tasks and with the task scheduler, the programs determine what trajectories a system takes through the forest of possible states.

Program Blocks

A program may be partitioned in a hierarchy of program blocks. Within a block, the program may introduce local assets that are used to support its operations. A program block is opened and closed by a block separator. For the externals of the block, the local assets are hidden.

Low-level and High-level Programs

The program that is meant here is a very low-level construct. It must not be interpreted as a high-level program that uses third or higher generation programming languages. However, every high-level language construct implies one or more of the described low-level language constructs. In fact, the operands in the low-level program correspond to the atomic operations that can be executed by the processing unit that is used by the current task. Similarly, the atomic path selectors correspond to the path selection that is implemented by the processing units.

Concurrent access

Concurrent access of assets or system resources can produce unexpected results. A write operation of a memory location may interfere with a read operation or a write operation on the same location by another thread. In order to circumvent such occasions a semaphore may be set that blocks other write operations during a read or write operation. It is also possible to temporary halt other threads by installing a critical section in the program that contains the read or write operation.

Blocking access and stopping threads may cause other artifacts such as deadlocks and race conditions.

Exchange of information between threads

Tasks that operate on different threads can exchange asset values or messages that contain commands by exploiting shared resources, such as shared memory. Systems connected by communication lines can communicate via serialization of asset values and commands. The receiver must de-serialize the received message. Communication can also take place within a task. In that case, there is no need for serialization. If the communication protocol requires reaction from the receiver, then there are two possibilities: synchronous communication and asynchronous communication. Synchronous communication means that the sender waits for the answer of the receiver. Asynchronous communication means that the sender proceeds without waiting for an answer. The answer is sent at a later instant. It can be sent to the original sender or it can be placed in a mailbox that is queried at regular instants by the original sender.


Communication is an action that makes use of a relation that exists between the sender and the receiver in order to exchange a command or the value of one or more assets between both ends of the relation. A relation of a subject with another subject is a special kind of asset. The communication between two subjects causes a series of state transitions at the receiver side. This series of state transitions is controlled by a program block. The start of a communication is also a special kind of trigger.


The values of assets that are exchanged during the communication are called ‘parameters’. The combination of the operation and the parameters is characterized as a ‘method’. The communication may result in an immediate callback. If during the callback only one parameter is transferred, then in software this parameter is called the ‘method result’. In that case, the callback is interpreted as part of the method. The trigger that causes the operation is called the ‘method call’.


In this terminology, communication from a subject to another subject consists of a method and a relation between the sender and the receiver of the transmitted command or message. The information in the command or message is contained in the kind of the method and in its parameters. It means that during the communication, the parameters of the method are transmitted from the sender to the receiver. The communication triggers an operation. The operation is controlled by a program block. That operation represents a sequence of state transitions in the receiver. During this process, the appearance of the receiver may change in a series of steps. In software, a direct callback that transfers a single parameter is considered part of the method. This callback will cause a single state-transition in the original sender.

Synchronous communication ends with the return of the method. Asynchronous communication means that the communication does not end with the return of the method.

Tasks and methods

A task may be implemented by a network of connected methods. In that case, the execution path of the task corresponds to a communication path that runs through the network. Detailed task scheduling then corresponds to the scheduling of commands and/or messages. In software, this is the normal way of implementing tasks.



Afgeronde rechthoek: Top of page Afgeronde rechthoek: Next page