Model checker aided design of a controller for a wafer scanner

ModelCheckerAidedDesignofaControllerfor

aWaferScanner󰀁

MartijnHendriks1,BarendvandenNieuwelaar2󰀇󰀇,andFritsVaandrager1

1NijmegenInstituteforComputingandInformationSciences,RadboudUniversityNijmegen,TheNetherlands{martijnh,fvaan}@cs.ru.nl,2DepartmentofMechanicalEngineeringEindhovenUniversityofTechnology,TheNetherlandsN.J.M.v.d.Nieuwelaar@tue.nl

Abstract.Foracase-studyofawaferscannerfromthesemiconduc-torindustryitisshownhowmodelcheckingtechniquescanbeusedtocompute(i)asimpleyetoptimaldeadlockavoidancepolicy,and(ii)aninfiniteschedulethatoptimizesthroughput.Deadlockavoidanceisstud-iedbasedonasimplefinitestatemodelusingSmv,andforthroughputanalysisamoredetailedtimedautomatonmodelhasbeenconstructedandanalyzedusingtheUppaaltool.TheSmvandUppaalmodelsareformallyrelatedthroughthenotionofastutteringbisimulation.Theresultswereobtainedwithintwoweeks,whichconfirmsoncemorethatmodelcheckingtechniquesmayhelptoimprovethedesignprocessofrealistic,industrialsystems.Methodologically,thecasestudyisinterest-ingsincetwomodels(andinfactalsotwomodelcheckers)wereusedtoobtainresultsthatcouldnothavebeenobtainedusingonlyasinglemodel(tool).

1Introduction

Schedulingandresourceallocationproblemsoccurinmanydifferentdomains,

forinstance(1)schedulingofproductionlinesinfactoriestooptimizecostsand

delays,(2)schedulingofcomputerprogramsin(real-time)operatingsystemsto

meetdeadlineconstraints,(3)schedulingofmicroinstructionsinsideaproces-

sorwithaboundednumberofregistersandprocessingunits,(4)schedulingof

trains(orairplanes)overlimitedquantitiesofrailwaytracksandcrossroads,and

(5)missionplanningforautonomousrobotsonspacecrafts.Typically,ineachof

thesedomainproblemsaresolvedusingdifferentapproachesandmathematical

tools.TheEUISTprojectAmetist(seehttp://ametist.cs.utwente.nl/)en-

visagesaunifyingframeworkfortime-dependentbehavioranddynamicresource

allocationthatcrossestheboundariesofapplicationdomains.

󰀁SupportedbytheEuropeanCommunityProjectIST-2001-35304(Ametist).󰀁󰀁Part-timesoftwarearchitectatASML,Veldhoven,TheNetherlands.IntheAmetistapproach,componentsofasystemaremodeledasdynamical

systemswithastatespaceandawell-defineddynamics.Allthatcanhappen

inasystemisexpressedintermsofbehaviorsthatcanbegeneratedbythe

dynamicalsystems;theseconstitutethesemanticsoftheproblem.Verification,

optimization,synthesisandotherdesignactivitiesexploreandmodifysystem

structuresothattheresultingbehaviorsarecorrect,optimal,etc.Preferably,

thelimitationsofcurrentlyknowncomputationalsolutionsshouldnotinfluence

modelingtoomuch:onlyafterthesemanticsofaproblemisproperlyunder-

stood,abstractionsandspecializationduetocomputationalconsiderationscan

intervene.Insuchsituations,thesoundnessofabstractionsshouldideallyalso

beproved,eitherviadeductiveverificationormodelchecking.

ThemissionofAmetististoextendthisapproach,whichunderliesthesuc-

cessfuldomainofformalverification,toresourceallocation,schedulingandother

time-relatedproblems.ThemathematicalcarrierfortheAmetistmethodology

isthetimedautomatonmodel[2,3],amodelingframeworkfordiscreteevent

dynamicalsystemsthatcanhandlequantitativetimingdelaysbetweenevents.

Sometoolsformodelcheckingtimedautomataalreadyexist,e.g.,Kronos[22]

andUppaal[13].Modelcheckingisamethodforformallyverifyingdynamical

systems.Specificationsaboutthesystemareexpressedastemporallogicfor-

mulas,andefficientsymbolicalgorithmsareusedtotraversethemodelandto

check(fullyautomatically)ifthespecificationholdsornot.Weaimatfurther

improvingmodelcheckingtoolsfortimedautomata,investigatingtheapplica-

bilityofthesetools,andestablishinglinkstotoolsdevelopedinspecificdomains

wheneverappropriate.

Inthispaper,asanillustrationoftheAmetistmethodology,weusemodel

checkingtechniquestosolvethedeadlockavoidanceandthroughputoptimiza-

tionproblemsforarealisticcaseofawaferscannerfromthesemiconductor

industry.

Amajorconcerninthedesignofcontrollersformanyresourceallocation

systems(RASs)isdeadlock,apermanentlyblockingcondition.Therearethree

generalwaysofhandlingdeadlock:(i)deadlockprevention,(ii)deadlockdetec-

tionandresolution,and(iii)deadlockavoidance.Deadlockpreventionrestricts

thesysteminsuchawaythatdeadlockisaprioriimpossible.Asaconsequence,

performancemaybeunnecessarilylow.Deadlockdetectionandresolution,on

theotherhand,isnotrestrictiveatallanddetectsandresolvesadeadlockat

run-time.This,however,maybeveryexpensive.Deadlockavoidanceachieves

amiddleground;itdynamicallychoosesthecontrolactionstoavoidtheoc-

currenceofdeadlock.Inthispaper,weshowhowaleastrestrictivedeadlock

avoidancepolicy(DAP)forthewaferscannercanbeeasilycomputedusing

Smv,amodelcheckerforfiniteautomata.ThisDAPcanberepresentedbya

veryshortpredicateoverthestatesofthewaferscanner,whichcanbeusedby

thecontrollerforthewaferscanner.

Inaddition,weusethetimedautomatontoolUppaaltodefinearefined

modelthataddstimingconstraintstoaddresstheissueofthroughputoptimiza-

tion.WerelatetheUppaalmodeltotheSmvmodelviatheconceptofstuttering