Linköping University: Students Alumni Trade and Industry/Society Internal Search
danka_lic

Towards Formal Verification in a Component-based Reuse Methodology

Daniel Karlsson

Licentiate Thesis No. 1058, Dept. of Computer and Information Science, Linköping University, December 2003

ABSTRACT
Embedded systems are becoming increasingly common in our everyday lives. As techonology progresses, these systems become more and more complex. Designers handle this increasing complexity by reusing existing components (Intellectual Property blocks). At the same time, the systems must still fulfill strict requirements on reliability and correctness.

This thesis proposes a formal verification methodology which smoothly integrates with component-based system-level design using a divide and conquer approach. The methodology assumes that the system consists of several reusable components. Each of these components are already formally verified by their designers and are considered correct given that the environment satisfies certain properties imposed by the component. What remains to be verified is the glue logic inserted between the components. Each such glue logic is verified PengQuasi-Static Scheduling for Multiprocessor Real-Time Systems with Hard and Soft TasksTechnical Report, Embedded Systems Lab, Dept. of Computer and Information Science, Linköping University, December 2003.We address in this report the problem of scheduling for multiprocessor real-time systems comprised of hard and soft tasks. We use utility functions associated to soft tasks that capture their relative importance and how the quality of results is influenced when a soft deadline is missed. The problem is thus finding a task execution order that maximizes the total utility and guarantees meeting the hard deadlines. We consider time intervals rather than fixed execution times for tasks. On the one hand, a single static schedule computed off-line is too pessimistic. On the other hand, a purely on-line approach, which computes a new schedule every time a task completes considering the actual conditions, incurs an overhead that is unacceptable due to the high complexity of the problem. We propose a quasi-static solution where a number of schedules are computed at design-time, letting only for run-time the selection of a particular schedule based on the actual execution times. We propose an exact algorithm as well as heuristics that tackle the time and memory complexity of the problem. We evaluate our approach through synthetic examples and a realistic application.


Related files:
danka_lic.pdfAdobe Acrobat portable document


[K03] Daniel Karlsson, "Towards Formal Verification in a Component-based Reuse Methodology", Licentiate Thesis No. 1058, Dept. of Computer and Information Science, Linköping University, December 2003
( ! ) perl script by Giovanni Squillero with modifications from Gert Jervan   (v3.1, p5.2, September-2002-)