Statechart BasedElevator Controller andIts Verification
S. GAberathnel, S. Devapriya Dewasurendra · 2006
Fordesigning modernautomation systems (event- driven complex reactive systems whichcontinuously react to external stimuli) itisnecessary todefine guidelines, methods andtools thatallow tocarryoutthedesigns within anoverall development methodology thatpermits tospecify these systems inaneasyandsafeway,tomaintain traceability alongthedifferent phases ofthedesign, andtohavethe neededknowledge aboutthebehaviors ofthedefined system. Basicissues related tocurrent specification technology have beendiscussed in(2). A methodology basedonstatecharts (1), (4)hasbeenproposed in(2)and(3) tobepresented inthe sameconference. Thecurrent paperdescribes thepresent status ofourworkinvalidating thismethodology onthe control ofanelevator system. An elevator systemisusually equipped withafairly large numberofsensors, makingita real-scale application, butsimpleenoughto servein demonstrating thebasicprinciples involved withclarity. Entire system isdesigned using state charts andimplemented in a Programmable logicdevice. To demonstrate the feasibility a prototype systemissimulated usingmicro controllers andtheresults arepresented inthepaper. However, inthis implementation, statecharts areonlyusedas formal specification ofcontrol whichprovides thebasis for functional decomposition oftheprograminto communicating Finite State Machines (FSM): portstructures proposed in(3) forreconfigurable implementation arenotyetincorporated. Hence, thecurrent paperdiscusses primary issues ofmodular controller implementation usingstatechart specifications. Verification hasbeendonebysimulating thecontroller on PIC16F877 MC inProteous 6forselected operations. Formal verification methodology of(3) will bevalidated inthenext stage ofthis research.