Simulation and Formal Verification for Improving Safety of PLC Programs

Recen Inno a ions in Mecha onics (RIiM) Vol. 3. (2016). No. 1-2. DOI: 10.17667/ iim.2016.1-2/9. Simula ion and Fo mal Ve i ica ion o Imp o ing Sa e y o PLC P og ams Joel Gal ão ME RICs Resea ch Cen e , Uni e si y o Minho Campus o Azu ém, 4800-058 Guima ães, Po ugal José Machado Mechanical Enginee ing Depa men , ME RICs Resea ch Cen e , Uni e si y o Minho Campus o Azu ém, 4800-058 Guima ães, Po ugal [email protected] Abs ac —The use o analysis echniques o imp o ing quali y o so wa e o indus ial con olle s is widely used. Mainly Simula ion and Fo mal Ve i ica ion can be used as complemen a y echniques imp o ing dependabili y o mecha onic sys ems beha io . In his pape he e a e used Simula ion and Fo mal Ve i ica ion o gua an eeing sa e so wa e o P og ammable Logic Con olle s, mainly ela ed wi h using Func ion blocks o IEC 61131-3 s anda d. Fo s udying, simula ing and e i ying beha io o hose blocks a e used imed au oma a, as modeling o malism, and UPPAAL, as ool o simula ion and Fo mal Ve i ica ion pu poses. Keywo ds—IEC 61131-3, Simula ion, Fo mal Ve i ica ion, Dependable Mecha onic Sys ems I. INTRODUCTION The e a e se e al echniques o analyses his ype o sys ems, bu Simula ion by MiL (Model-in- he-Loop) and Fo mal Ve i ica ion by Model Checking [1] wo possible me hods o achie e he aim secu e command speci ica ion [2]. Same esea che s belie e ha Simula ion is conside ably be e because is possible o s udy i he de eloped code e ec i ely pe o m he ask needed, and i necessa y ealize same co ec ions acco ding o he needs. Al hough was same disad an ages [3], such as, jus a pa o he domain o possible beha iou s o he con olle is es ed. One he o he hand, he o mal e i ica ion by Model Checking echniques make possible o es i he de eloped sys em espond o he p ojec speci ica ions in all he domain o possible beha iou s o he con olle , and he con olle ne e each a deadlock s a e, and is has been said ha model checking is he only know me hod o ensu e ha he code is wi hou any e o [4]. Ne e heless, was he need o use logic ha same conside di icul o u ilize and unde s and [5]. The wo echniques (Simula ion by MiL and Fo mal Ve i ica ion by Model Checking) he g anula i y o he models is e y impo an . This ac leads o he objec i e o his esea ch, ha ocuses on de eloping models o he beha io o he unc ion blocks de ined by he s anda d IEC 61 131-3 [6], aking in o accoun a me hodology ha combines he ad an ages o Simula ion by MiL and Fo mal Ve i ica ion by Model Checking using he same models, o allow a mo e ca e ul sa e y analysis o he command speci ica ion o PLC (P og ammable Logic Con olle s). Conside ing simula ion, one o he pionee s in his a ea is he wo k p oposed by Ba esi in 1997 [7]. The e a e same comme cial so wa e’s like A ena and Au oMod, bu his applica ions conside li le abou he logic behind he con ol he e o hey canno be e ec i ely used o es command speci ica ions [8]. The pape p esen ed by e e ence [9], ha demons a es a echnique o simula e and isual e i y, ha begins wi h he code w i en in Ladde Diag am, one o he IEC 61 131-3 languages, using ini e s a e au oma a [10]. The e a e se e al wo ks [7] [11] ha use he o malism Disc e e E en Sys em Speci ica ion [12], his wo ks y o educe he ime need o simula e a sys em. In [7] hey p esen an in e se me hodology ha uses da a om ime-s amped signal his o y and a PLC inpu /ou pu signal able ex ac ed om he exis ing p oduc ion sys em o c ea e he simula ion models. In he o he hand he a icle [11] demons a e he ad an ages o using empla es o gene a e de models. In he poin o iew o Fo mal Ve i ica ion by Model Checking, his me hod was i s applied o con ol sys ems by Moon in 1992 [13]. This echnique was hem u ilized by a g ea deal o au ho s, bu he o malisms used o speci y he sys em beha io , he me hod he p ope ies a e w i en and he applica ions used a e di e en [14][15] [16] [17] [18][19] The wo k g oup o e e ence [20] p esen in es iga ion using NuSMV [21]. The p ope ies a e speci ied in compu a ion ee logic[22] o Linea Tempo al Logic [23] , and he code is w i en in S uc u ed Tex , o he o he IIEC 61 131-3 languages. The wo k ocus on he modula ion o ime in a ealis ic manne , o accomplish ha hey de eloped models o he unc ion block TON (Time ON delay) de ined by he IEC 61 313-3 s anda d [6]. O he echnique is p oposed by [24], again using model checking based in models c ea ed in BIP (Beha io , Recen Inno a ions in Mecha onics (RIiM) Vol. 3. (2016). No. 1-2. DOI: 10.17667/ iim.2016.1-2/9. In e ac ions, P io i ies) [25]. In his a icle a e p oposed models o he P og am O ganiza ion Uni de ine by he IEC 61 131-3 [6] s anda d, once mo e wi h especial a en ion o he unc ion block TON. To e i y p ope ies is used he D-Finde [26], ha allow de ec ing deadlock and o he ype o beha iou s. This echniques do no conside ime cons ain s, ha u n he analyses limi ed [27]. The in es iga o s in [28] p opose a me hodology ha uses p og am code w i en in sequen ial unc ion cha s , ano he o he IEC 61 131-3 languages, ha is han con e ed o Timed Au oma a [29] and om he p ojec speci ica ions a e o mula ed a i ma ions o e i y in he models u ilizing TCTL (Timed Compu a ion T ee Logic) [30] (Fig. 1). All he p ocess o he modula ion o he e i ica ion a e ealized on he applica ion UPPAAL [31]. They p opose a model o he unc ion block TON, because hey conside he modula ion o he con olle beha iou has o be as close as possible o wha happens in he equipmen s. On he o he hand e e ence [32] p opose a echnique o con e code w i en in Func ion Blocks Diag am o Timed Au oma a we e hey conside models o he P og am O ganiza ion Uni s mo e pa icula ly unc ions and unc ion blocks. In his pape is conside ed a me hodology o make sa e y analyses o command speci ica ion o indus ial con olle s, mo e p ecisely PLC ha ies o combine de ad an ages o simula ion and o mal e i ica ion, using o desc ibe he beha iou s o mecha onic sys em he o malism imed au oma a in he applica ion UPPAAL, as displayed in Fig. 1. Fig. 1. Analyses me hodology applied in his pape Fo his app oach, i is conside ed he speci ica ion de eloped in SFC (Sequen ial Func ion Cha ). Also, he me hodology o c ea ing he global model o he sys em in Timed Au oma a, o simula ion and o mal e i ica ion pu poses is p oposed. In o de o achie e he goals p oposed o his wo k, his pape is o ganised as ollows: sec ion 2 p oposes a case s udy, illus a ing he app oach and, also p esen s he o mal con olle ’s speci ica ion aking in o accoun he in ended beha iou o he sys em; sec ion 3 deals wi h some wo k hypo hesis, mainly conce ning he ansla ion o he speci ica ion o imed au oma a, in o de o achie e he ask o simula ion and o mal e i ica ion, using he UPPAAL so wa e; and, inally, he e a e p esen ed some conclusions and u u e wo k, in sec ion 4. II. CASE STUDY A. Speci ica ion o he con olle In his wo k, he au oma ic sys em used as case s udy is a ca ba ie , o be used in pa king lo , schema ically ep esen ed in Fig. 2. This au oma ic sys em is ac ua ed by one mo o wi h wo di ec ions o mo emen : one con ols he mo emen wi h di ec ion “up” (M_UP) and ano he con ols he mo emen wi h di ec ion “down” (M_D). Besides ha , he sys em has a se o senso s: one de ec s he p esence o one ca a a ime (s1) and wo o he senso s de ec he ba ie posi ion, “s_up” on he up posi ion and “s_d” on he down posi ion Fig. 2. Schema ic ep esen a ion o he ca ba ie , wi h espec i e senso s and ac ua o s. The inpu a e: he senso “si” esponsible o de ec s p esence o ca ; he senso “s_up” ha de ec s he ba ie in he up posi ion up; and he senso s_down ha has he ask o de ec he down posi ion o he ba ie . In he o he hand, he sys em was o ou pu ha a e he o de s o open he ba ie (M_UP), and o close i (M_D). The con olle beha io a e: when appea s a ca , he ba ie mus mo e up and when disappea s he ca , he ba ie mus mo e down. I , in some momen , a new ca appea s he ba ie mus go up and so on. This in ended beha io is desc ibed on he Fig. 2 o malized by a SFC. Consequen ly, when is no ca de ec ed in senso he ba ie mus be closed (co esponding o down posi ion) ha co esponds o he ini ial posi ion conside ed o he sys em. This way, all he Boolean condi ions associa ed o all he ansi ions o his model co espond o ising o alling edges o he men ioned senso s. I is in ended ha his speci ica ion be implemen ed in a PLC, which p og am will be w i en conside ing Ladde language and Func ions blocks p oposed in IEC 61131-3 [6] Because his wo k is de o ed o he p esen a ion and e i ica ion o he beha io co esponden o ising and alling Recen Inno a ions in Mecha onics (RIiM) Vol. 3. (2016). No. 1-2. DOI: 10.17667/ iim.2016.1-2/9. edges, his subjec will be ea ed wi h ocused special a en ion. Fig. 3. Sequen ial Func ion Cha s o he compo men desc ibed be o e. B. T ansla ion o he con olle speci ica ion o Ladde and Func ion blocks The ansla ion o he p esen ed speci ica ion, o PLC p og amming language de ined in [6], conside s wo dis inc pa s: one conce ns he ansla ion o he dynamics o he model acco ding me hodology p oposed in [2]. Conce ning he beha io o he ising and alling edges he e a e conside ed he espec i e compo men de ined on he s anda d. In his case, he beha io in ended is as ollows: he e a e wo edge de ec ion ypes, one used o ansi ion o he logic alue 0 o 1 ( ising edge), and o he ha does he opposi e eco ding ( alling edge). To model his, he ising edge beha io is desc ibed in Fig.4. LOCK FUNCTION_B END_ CLK := MEM MEM NOT ANDCLK := Q END_VAR 0= :BOOL : MEM VAR_RETAIN END_VAR BOOL : Q VAR_OUTPUT END_VAR BOOL :CLK VAR_INPUT R_TRIG LOCK FUNCTION_B Fig. 4. Rising edge beha io [6] . The code demons a es ha i inpu signal (“CLK”), ha ep esen s he a iable ha is in ended o be eco ded, he s a e changes, he e is an in e nal a iable (“MEM”) ha keeps he alue o “CLK” in e e y scan cycle. Tha in o ma ion is no was ed because is ecycled in he ou pu (Q) calcula ion in he nex PLC scan cycle. When “Q” has he logic alue 1 means ha he “CLK” has made he ising edge changeo e [6]. Ne e heless, some imes he eco ding need is di e en . Some cases he need is o eco d he momen whe e a signal changes om Boolean alue 1 o 0. This co esponds o he si ua ion co esponding o he alling edge, which beha io is desc ibed and p esen ed in Fig. 5. LOCKFUNCTION_B END_ CLK NOT := MEM MEM NOT ANDCLK NOT := Q END_VAR 1= :BOOL : MEM VAR_RETAIN END_VAR BOOL : Q VAR_OUTPUT END_VAR BOOL :CLK VAR_INPUT F_TRIG LOCK FUNCTION_B Fig. 5. Falling edge beha io [6]. In his case he code is made o sa ing he momen when a iable ha we wan o s udy changes om de logic alue 1 o 0. As in he ising edge he e is one inpu (“CLK”), one memo y a iable (MEM), bu his ime eco ds he nega ion o CLK e e y PLC scan cycle. When CLK and MEM a e ze o, Q will be one. This has meaning ha he analyzed a iable changed om one o ze o. Conce ning he speci ica ion p esen ed in Fig. 3, he e a e conside ed bo h ising and alling edges. This way, hose Boolean alues will be calcula ed as demons a ed abo e. III. SIMULATION AND FORMAL VERIFICATION OF THE SPECIFICATION In o de o pe o m he simula ion and o mal e i ica ion i was ollowed he app oach p oposed in o he ansla ion o SFC o Timed Au oma a (TA) [33], o ob aining he imed au oma a model. Also, i has been conside ed he modeling o he compo men o he con olle . Fo his, a modula me hod has been ollowed o ob aining he global model o be simula ed and o mally e i ied in UPPAAL. The simula ion echniques can be classi ied by SiL (So wa e-in- he-Loop), MiL, HiL (Ha dwa e-in- he-Loop), and LT (labo a o y es ing). Recen Inno a ions in Mecha onics (RIiM) Vol. 3. (2016). No. 1-2. DOI: 10.17667/ iim.2016.1-2/9. Fig. 6. Simula ion ecniques All hese simula ion echniques ha e he pa icula i y o no es all he space beha io o he con olle , making i impossible o asse i s e ec i eness o one hund ed pe cen . In his in es iga ion, is conside ed a simula ion echnique using models (MIL), ei he he p og am o o he physical pa o mecha onic closed-loop sys em. This echnique is gene ally used in ea ly phases o de elopmen o new p ocess equipmen . No need o special equipmen , jus a e cheape han be o e. When de eloped in an app op ia e en i onmen , and be able o simula e, i is also easible o e i ica ion by model checking, which ensu es analysis o all he con olle beha io space. The models a emp o in e ac wi h each o he in he same way as mecha onic sys ems in e ac in eali y. In o de o achie e his pu pose, a cha ge model is equi ed o manage he o de in which hey a e execu ed and how hey in e ac . Fi s , he e a e wo majo g oups o models, ep esen ing he beha io o he PLC and a g oup which eac as in he p ocess. The in e ac ion be ween he wo pa s o he model is made h ough a iables. he p ocess a iables e e y PLC cycle a e assigned o he in e nal a iables o he con olle , and his da a will un i s in e nal code, which will calcula e he ou pu s. This in o ma ion is again ansmi ed o he p ocess con olle h ough he alloca ion o a iables o hei co esponding alues o he p ocess. I mus be highligh ed ha he main p oblem o pe o ming simula ion and o mal e i ica ion is no he c ea ion o he modules ha compose he global model in TA, bu he synch oniza ion o he e olu ion o he modules. This is because i mus be conside ed he in e nal PLC scan and he changing o he logical alues o he a iables mus be gua an eed acco ding he co ec unc ioning o he PLC. Fo his pu pose i was c ea ed a model o he managemen o all o he modules, in o de o gua an ee he in ended co ec e i ica ion. The modelling o all sys em, in one only module, is no achie able and canno be p oposed as a me hodology o sol ing p oblems o his kind. In o de o illus a e he model p oposed o he ising and alling edges is p esen ed, in igu e 5 he TA model o he ising edge and alling edge o he senso s1. Fig. 1. Rising edge and alling edge models, o he senso s1, de eloped in TA, o be o mally e i ied wi h UPPAAL. These modules (one o each edge) co espond o he beha io s p esen ed in igu es 3 and 4, espec i ely [25].The alues ha a e assigned o he a iables a e di ec ly ob ained om wha is desc ibed in hose igu es, bu ano he a iable (synch oniza ion message “FB_E”) is conside ed in he model. In ac , he synch oniza ion, ha is possible o see in he model o igu e 5, is necessa y due o he synch oniza ion o he e olu ion o all models conside ed in he global model. Figu e 6 illus a es he exis ing ela ion be ween some modules conside ed o he global model o he sys em. Fig. 2.Schema ic synch oniza ion be ween modules o he global TA model, used in UPPAAL, o o mal e i ica ion pu poses. In ac , his ela ion be ween he modules makes possible ha he alues o a iables a e ob ained in he equi alen momen s ha hey co espond o he dynamics o he p og am execu ion in a PLC. Figu e 7 illus a es how i has been de eloped wi h pa s o each module conside ed in igu e 6. Recen Inno a ions in Mecha onics (RIiM) Vol. 3. (2016). No. 1-2. DOI: 10.17667/ iim.2016.1-2/9. Fig. 3. Illus a ion o synch oniza ion be ween modules o he global TA model, used in UPPAAL, o o mal e i ica ion pu poses. Le ’s explain how he model has been de eloped in o de o accomplish he desi ed beha io o he Func ion blocks conside ed ( he ising and alling edges). A beginning, when he model s a s i s e olu ion, he ini ial loca ion o he module 1 (manage o all modules, igu e 7) s a s e olu ion and sends a synch oniza ion message o module 2. Module 2 models he beha io o he con olle ( igu e 7) and he ecei ed message om manage module allows s a ing he espec i e e olu ion. I has been conside ed a mono ask and sequen ial con olle wi h, a leas , h ee s eps in he scan cycle: inpu s eading, p og am execu ion and ou pu s upda ing. A e he s ep inpu s eading, on he model 2, be pe o med his module sends a message (START_PE) o model 3 ha will be esponsible o he s a ing o he p og am e olu ion model. The beginning o he e olu ion o he module co esponding o he p og am o he PLC has se e al s eps, bu he i s one conside ed is he s ep conce ning he calcula ion o he alues co esponding o he modules o he ising and alling edges (module 4, igu e 7). This e olu ion will occu in his p ecise momen and ne e mo e du ing he model e olu ion, unless ha a new cycle o he PLC happens again. When he e olu ion o he p og am ends, his is sen a message o he module co esponding o he PLC beha io , in o de o be upda ed he ou pu s. A e his, he e olu ion o he model is done by allowing e olu ion o he modules co esponding o he physical plan models. IV. CONCLUSION When de eloping a con olle speci ica ion, he changing o logical alue o disc e e beha io a iables is one o mos common needs o modeling, namely he ising edge and aLling edge o a Boolean a iable. The implemen a ion o his beha io , in indus ial con olle s, mo e p ecisely in p og ammable logic con olle s is by using IEC 61131-3 unc ion blocks. This means ha he simula ion and o mal e i ica ion o he speci ica ion o he desc ibed beha io s is one o he mos impo an asks, in o de o ob ain sa e and eliable con olle s’ so wa e o be implemen ed in physical con olling de ices, such as p og ammable logic con olle s o o he s, commonly used in indus y. Wi h his global modeling app oach, i is possible o conside he beha io o con olle s’ a iables in a e y ealis ic way, ob aining a global model o be simula ed and e i ied. This global model conside s, also, he beha io o he plan , allowing o p o e mo e beha io p ope ies o he sys em. The use o UPPAAL an imed au oma a o malism, making possible o ake he modeling o ime in o accoun , is c ucial when models o he plan a e conside ed because physical componen s beha e in a non-de e minis ic way and always i is needed o conside hei e olu ion in ime. Fu u e wo ks in his domain will conside con olled dis ibu ed sys ems and de ails on modelling hose sys ems, mainly because o mo e o less complexi y o he espec i e con olle s. ACKNOWLEDGMENT The au ho s a e g a e ul o ME RICs Resea ch Cen e Suppo o ealiza ion o his p ojec . REFERENCES [1] E. Cla ke, A. Bie e, R. Raimi, and Y. Zhu, “Bounded model checking using sa is iabili y sol ing,” Fo m. Me hods Sys . Des., ol. 19, no. 1, pp. 7–34, 2001. [2] J. M. R. Gal ão, “Con e são sis emá ica do compo amen o de inido nos blocos uncionais da no ma IEC 61 131-3 pa a au óma os ini os empo izados,” Uni e si y o Minho, 2015. [3] J. J. T. Kleijn, M. A. Renie s, and J. E. Rooda, “Analysis o an indus ial sys em,” Fo m. Me hods Sys . Des., ol. 22, no. 3, pp. 249–282, 2003. [4] Y. Zhang, Y. Dong, H. Hong, and F. Zhang, “Code Fo mal Ve i ica ion o Ope a ion Sys em,” In . J. …, ol. 2, no. Decembe , pp. 10–18, 2010. [5] J. Campos and J. Machado, “A Speci ica ion Pa e ns Sys em o Disc e e E en Sys ems Analysis,” In . J. Ad . Robo . Sys ., ol. 10, p. 1, 2013. [6] In e na ional Elec o echnical Commission, “IEC In e na ional S anda d IEC 61131-3,” P og am. Con ol., ol. Pa 3, 2003. [7] S. C. Pa k, M. Ko, and M. Chang, “A e e se enginee ing app oach o gene a e a i ual plan model o PLC simula ion,” In . J. Ad . Manu . Technol., ol. 69, no. 9–12, pp. 2459–2469, 2013. [8] L. Ba esi, S. Ca meli, A. Mon i, and M. Pezzè, “PLC p og amming languages: A o mal app oach,” P oc. Au om., ol. 98, 1998. [9] C. M. Pa k, S. M. Bajimaya, S. C. Pa k, G. N. Wang, J. G. Kwak, K. H. Han, and M. Chang, “De elopmen o i ual simula o o isual alida ion o PLC p og am,” in Compu a ional In elligence o Modelling, Con ol and Au oma ion, 2006 and In e na ional Con e ence on In elligen Agen s, Web Technologies and In e ne Recen Inno a ions in Mecha onics (RIiM) Vol. 3. (2016). No. 1-2. DOI: 10.17667/ iim.2016.1-2/9. Comme ce, In e na ional Con e ence on, 2006, p. 32. [10] A. Clee emans, D. Se an-Sch eibe , and J. L. McClelland, “Fini e s a e au oma a and simple ecu en ne wo ks,” Neu al Compu ., ol. 1, no. 3, pp. 372–381, 1989. [11] M.-S. Ko, D. Chang, G.-N. Wang, and S. C. Pa k, “The Templa e Model App oach Fo PLC Simula ion In An Au omo i e Indus y.,” in ECMS, 2012, pp. 306–312. [12] B. P. Zeigle , “DEVS ep esen a ion o dynamical sys ems: E en - based in elligen con ol,” P oc. IEEE, ol. 77, no. 1, pp. 72–80, 1989. [13] I. Moon, G. J. Powe s, J. R. Bu ch, and E. M. Cla ke, “Au oma ic e i ica ion o sequen ial con ol sys ems using empo al logic,” AIChE J., ol. 38, no. 1, pp. 67–75, 1992. [14] H. Guéguen and J. Zay oon, “On he o mal e i ica ion o hyb id sys ems,” Con ol Eng. P ac ., ol. 12, no. 10, pp. 1253–1267, 2004. [15] J. M. Machado, “In luence de la p ise en comp e d’un modèle de p ocessus en é i ica ion o melle des Sys èmes à E énemen s Disc e s,” Uni e sidade do Minho, 2006. [16] N. Sha ygina, J. B owne, F. Xie, R. Ku shan, and V. Le in, “Lessons lea ned om model checking a NASA obo con olle ,” Fo m. Me hods Sys . Des., ol. 25, no. 2–3, pp. 241–270, 2004. [17] E. M. Hahn, A. Ha manns, H. He manns, and J.-P. Ka oen, “A composi ional modelling and analysis amewo k o s ochas ic hyb id sys ems,” Fo m. Me hods Sys . Des., ol. 43, no. 2, pp. 191– 232, 2013. [18] R. Passe one, J. R. Bu ch, and A. L. Sangio anni-Vincen elli, “Re inemen p ese ing app oxima ions o he design and e i ica ion o he e ogeneous sys ems,” Fo m. Me hods Sys . Des., ol. 31, no. 1, pp. 1–33, 2007. [19] S. Nadjm-Teh ani and J.-E. S ömbe g, “Fo mal e i ica ion o dynamic p ope ies in an ae ospace applica ion,” Fo m. Me hods Sys . Des., ol. 14, no. 2, pp. 135–169, 1999. [20] B. F. Adiego, D. Da as, E. B. Vinuela, J.-C. Tou nie , V. M. G. Suá ez, and J. O. Blech, “Modelling and Fo mal Ve i ica ion o Timing Aspec s in La ge PLC P og ams,” in P oc. o IFAC Wo ld Cong ess, 2014. [21] A. Cima i, E. Cla ke, F. Giunchiglia, and M. Ro e i, “NuSMV: A new symbolic model e i ie ,” in Compu e Aided Ve i ica ion, 1999, pp. 495–499. [22] T. Ha e and W. Thomas, “Compu a ion ee logic CTL* and pa h quan i ie s in he monadic heo y o he bina y ee,” in Au oma a, Languages and P og amming, Sp inge , 1987, pp. 269–279. [23] P. Wolpe , “Tempo al logic can be mo e exp essi e,” In . Con ol, ol. 56, no. 1, pp. 72–99, 1983. [24] R. Wang, Y. Guan, L. Liming, X. Li, and J. Zhang, “Componen - based o mal modeling o PLC sys ems,” J. Appl. Ma h., ol. 2013, 2013. [25] A. Basu, M. Bozga, and J. Si akis, “Modeling he e ogeneous eal- ime componen s in BIP,” in So wa e Enginee ing and Fo mal Me hods, 2006. SEFM 2006. Fou h IEEE In e na ional Con e ence on, 2006, pp. 3–12. [26] S. Bensalem, M. Bozga, T.-H. Nguyen, and J. Si akis, “D- inde : A ool o composi ional deadlock de ec ion and e i ica ion,” in Compu e Aided Ve i ica ion, 2009, pp. 614–619. [27] M. Zhou, H. Wan, R. Wang, X. Song, C. Su, M. Gu, and J. Sun, “Fo mal componen -based modeling and syn hesis o PLC sys ems,” Compu . Ind., ol. 64, no. 8, pp. 1022–1034, 2013. [28] M. Pe in and J.-M. Fau e, “Building meaning ul imed models o closed-loop DES o e i ica ion pu poses,” Con ol Eng. P ac ., ol. 21, no. 11, pp. 1620–1639, 2013. [29] R. ; Alu and D. Dill, “Au oma a o modeling eal- ime sys ems,” P oc. se en een h In . Colloq. Au om. Lang. P og am., pp. 322–335, 1990. [30] R. Alu , C. Cou coube is, and D. Dill, “Model-checking in dense eal- ime,” In . Compu ., ol. 104, no. 1, pp. 2–34, 1993. [31] K. G. La sen, P. Pe e sson, and W. Yi, “Uppaal in a Nu shell,” In . J. So w. Tools Technol. T ans ., ol. 1, no. 1, pp. 134–152, 1997. [32] E. P. Enoiu, D. Sundma k, and P. Pe e sson, “Model-based es sui e gene a ion o unc ion block diag ams using he uppaal model checke ,” in So wa e Tes ing, Ve i ica ion and Valida ion Wo kshops (ICSTW), 2013 IEEE Six h In e na ional Con e ence on, 2013, pp. 158–167. [33] M. Uzam, “A gene al echnique o he PLC-Based implemen a ion o RW supe iso s wi h ime delay unc ions,” In . J. Ad . Manu . Technol., ol. 62, no. 5–8, pp. 687–704, 2012