| De groep Systems Engineering van de Faculteit Werktuigbouwkunde ontwikkelde tien jaar geleden de modelleertaal X. In X kan een model worden gemaakt van een fabricagesysteem (een fabricagelijn van een fabriek of een afzonderlijke machine). Zo'n model kan dan, met behulp van tools, worden geanalyseerd, en met het zo verkregen inzicht in het dynamisch gedrag van het gemodelleerde fabricagesysteem kan het vervolgens worden verbeterd. Op dit moment gaat die analyse voornamelijk door middel van simulatie. Daarmee kunnen performance-aspecten (zoals 'throughput' en 'flow time') worden geanalyseerd, maar de garantie dat het functionele gedrag van een systeem correct is, kan er niet mee worden verkregen. Immers, middels simulatie kan de aanwezigheid van fouten worden vastgesteld, maar nooit de afwezigheid van fouten. Een geschikte manier om wel garantie over het correct functioneren te verkrijgen is via formele methoden: wiskundige technieken om te redeneren over de correctheid van systemen. Het doel van het TIPSy project is om performance analyse en formele verificatie te combineren. Er wordt getracht om X te integreren met bestaande formele methoden; dit vergt aanpassingen van deze methoden. Er zullen mogelijkerwijs ook nieuwe formele methoden moeten worden ontwikkeld voor X. Het project wordt uitgevoerd aan het hand van aantal cases. Er wordt begonnen met de bestudering van de performance en het functionele gedrag van simpele machines, maar het is de bedoeling dat er uiteindelijk wordt gerekend aan de complexe systemen die ASML produceert ten behoeve van de halfgeleiderindustrie. |
