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