16423

14633

كارشناسي ارشد

نرم افزار

اصفهان : دانشگاه صنعتي اصفهان

1399

سيزده، 87ص.: مصور، جدول، نمودار

الهام محمود زاده، علي ابن نصير

مريم موزراني، زينب زالي

1399/11/20

كتابنامه

مهندسي كامپيوتر

مهندسي برق و كامپيوتر

1400/02/13

2657267

Model Extraction and Veri cation of Contiki s Scheduling Algorithm Hassan Mousavi h mousavi@ec iut ac ir July 2020 Department of Electrical and Computer Engineering Isfahan University of Technology Isfahan 84156 83111 Iran Degree M Sc Language Farsi Under supervison of Dr Elham Mahmoudzadeh Dr Ali EbnenasirAbstract Today the Internet of Things IOT and Cyber Physical Systems CPS are widely used For the systems with criticalfunctionalities the reliability is of particular importance On the other hand due to the high interaction of the systems withhardware how to manage interrupts memory limitations and light weight of operations should be considered One of themost used operating systems in this eld is Contiki In fact Contiki is a lightweight open source operating system in C Inaddition high portability and the ability to run on a variety of platforms and event oriented features are also important featuresof Contiki In this project we have analyzed one of the most critical components of Contiki called the scheduling algorithmand then formally reviewed it To this end rst we have analyzed the scheduling algorithm source code and also the interactionwith other parts of the operating system in detail Also we have driven a state machine based abstraction of the scheduler smodes of operation along with the control ow abstractions of the scheduler s most important functions Meanwhile in thecurrent research abstract models of process process list event and event queue which are the most important coordinationstructures of scheduling functions are presented We then have extracted a set of transformation rules to generate the formalspeci cations of the scheduler in Promela and accordingly the Promela model is generated After that expected propertiesof the proper functionality of scheduler are analyzed and then converted into formal Linear Time Logic formulas Finally theformulas are applied to the Contiki scheduler algorithm using SPIN model checker and formally veri ed As a result in thisproject three aws were found in the Contiki s scheduler and accordingly the source code are xed Key Words Model extraction Formal veri cation Contiki Scheduler Promela

الهام محمود زاده، علي ابن نصير

مريم موزراني، زينب زالي