Time: Tuesday 27.1.2004, 14:30
Place: Room D2-106, Fr. Bajersvej 7
The talk focuses on work in progress on synchronous systems containing buffers, registers and memory interconnected by several shared and proprietary busses. The concrete example is based on a radar system memory interface case study from the IST AMETIST project. The analysis of this system concentrates on the problems related to concurrency, in particular, on how to manage the shared resources in such a way that the system operates correctly. The contribution of the work is a way to partition the problem into independent subproblems that enable to abstract away details that are irrelevant with respect to the concurrency issues while still guaranteeing correct behaviour in the concrete system. This is necessary to make the problem solvable by a model checker.