Software engineering - 3 (SIS-3) SIS-3 addresses theoretical and implementation issues in the
context of complex embedded systems composed of multiple concurrently
executing software components. The course starts with an introduction
into real-time systems architecture, real-time kernel organization
and principles of operation. It proceeds with a detailed discussion
of key issues, such as task management and scheduling in a hard
real-time environment, time management (i.e. timing event generation
and processing), external event management, task synchronization
and communication. The insight and experience gained during that
part of the course is ultimately used to present formal models
(frameworks) specifying relevant aspects of complex real-time
systems, such as system structure, subsystem/component behaviour
and interaction. These models and associated design methods can
be used to systematically develop advanced embedded applications,
e.g. hierarchical and distributed computer control systems, complex
man-machine systems, etc.
Formal verification technique, as an integral part of the design
cycle, is increasing in importance for correctness assurance of
embedded systems. It allows the designer to verify that a mathematical
model of a system satisfies its abstract logical specification.
Model checking is a formal verification technique based on exhaustive
state space exploration of the model of a finite state system
(FSM). Given an input FSM model and a property in temporal logic,
a model checker determines whether the property holds in the model,
and returns with a counterexample trace in case the property fails.
Advanced issues from SIS2 are delivered, and SMV together with
already known tools (SPIN, UPPAAL, Timestool) are used in practical
projects. To achieve the high level of confidence in the correctness
required in a safety-critical embedded system, other methods are
studied, like symbolic simulation and testing.
Course form SIS 3: Semester course with lectures, project assignments
and laboratory experiments.
Teachers: Professor Christo Angelov
Assistant Professor Nicolae Marian.
Books 1. C.K. Angelov, Lecture Notes in Embedded Software Engineering,
Mads Clausen Institute for Product Innovation, 2003.
2. N. Marian, Lecture Notes in Model Based Design and Verification
for Embedded Software, Mads Clausen Institute for Product Innovation,
2003.
3. J.L. Labrosse, MicroC OS II: The Real-Time Kernel (With CD-ROM),
CMP Books, 2002, ISBN: 1578201039.
4. E.M. Clarke, O. Grunberg, D.A. Peled, Model Checking, MIT Press,
2001, ISBN: 0-262-03270-8.