Weizmann Contributions to AMETIST, Year 1
Bibtex entries of the publications
- Optimal Scheduler for a Memory Card (Terma
This report describes a scheduler synthesis for
the memory interface card offered by Terma as a case study for the AMETIST
consortium. A model of the system in the SMV
modeling language is introduced. This model can be used to produce valid schedules
for systems with small number of buffers. A method to synthesize an optimal
(in terms of buffer sizes) scheduler for the full system is also given. The
schedule is verified by the SMV
model checker using the above- mentioned model. Some extensions to cards with
other parameters are discussed.
smart-card personalization machine with LSCs
LSCs modeling and
is a formal graphical language originally proposed for software specifications.
We show that LSCs
provide natural modeling language for systems such as the smart-card personalization
is taken as an example of a scenario based specification language which enables
better modeling procedure using the Play-In/Play-Out
approach. We also demonstrate that it is possible to synthesize a scheduler
with Smart Play-Out.
Created by: Gera Weiss
Updated by: Angelika Mader Last change: May 22, 2003