Promela Formal Modelling and Verification of IEC 61499 Systems with comparison to SMV

Viktor Shatrov; Valeriy Vyatkin

doi:10.1109/INDIN45523.2021.9557513

Promela Formal Modelling and Verification of IEC 61499 Systems with comparison to SMV

ITMO University

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussa › Conference article in proceedings › Scientific › vertaisarvioitu

1 Sitaatiot (Scopus)

125 Lataukset (Pure)

Abstrakti

This paper presents a method of formal modelling of IEC 61499 systems of Function Blocks with Promela¹. The existing method of formal verification of IEC 61499 using SMV (Symbolic Model Verifier) is compared with a new approach of verification using SPIN² which is an explicit-state model-checker. The performance of both approaches is studied using a set of deterministic systems of multiple computational units as an example and a more complex non-deterministic elevator model.

Alkuperäiskieli	Englanti
Otsikko	2021 IEEE 19th International Conference on Industrial Informatics (INDIN)
Kustantaja	IEEE
Sivut	1-6
Sivumäärä	6
ISBN (elektroninen)	978-1-7281-4395-8
ISBN (painettu)	978-1-7281-4396-5
DOI - pysyväislinkit	https://doi.org/10.1109/INDIN45523.2021.9557513
Tila	Julkaistu - 11 lokak. 2021
OKM-julkaisutyyppi	A4 Artikkeli konferenssijulkaisussa
Tapahtuma	IEEE International Conference on Industrial Informatics - Palma de Mallorca, Spain, Palma de Mallorca, Espanja Kesto: 21 heinäk. 2021 → 23 heinäk. 2021 https://2021.ieee-indin.org/

Conference

Conference	IEEE International Conference on Industrial Informatics
Lyhennettä	INDIN
Maa/Alue	Espanja
Kaupunki	Palma de Mallorca
Ajanjakso	21/07/2021 → 23/07/2021
www-osoite	https://2021.ieee-indin.org/

Pääsy asiakirjaan

10.1109/INDIN45523.2021.9557513

ELEC_Shatrov_etal_Promela_Formal_Modelling_IEEE_INDIN_2021Accepted author manuscript, 611 KB

Muut tiedostot ja linkit

Linkki julkaisuun Scopuksessa

Siteeraa tätä

@inproceedings{e6c8c9584dcc4914b7a4f841b68afa0b,

title = "Promela Formal Modelling and Verification of IEC 61499 Systems with comparison to SMV",

abstract = "This paper presents a method of formal modelling of IEC 61499 systems of Function Blocks with Promela1. The existing method of formal verification of IEC 61499 using SMV (Symbolic Model Verifier) is compared with a new approach of verification using SPIN2 which is an explicit-state model-checker. The performance of both approaches is studied using a set of deterministic systems of multiple computational units as an example and a more complex non-deterministic elevator model.",

keywords = "Performance evaluation, Computational modeling, Memory management, XML, Tools, Elevators, IEC Standards",

author = "Viktor Shatrov and Valeriy Vyatkin",

year = "2021",

month = oct,

day = "11",

doi = "10.1109/INDIN45523.2021.9557513",

language = "English",

isbn = "978-1-7281-4396-5",

pages = "1--6",

booktitle = "2021 IEEE 19th International Conference on Industrial Informatics (INDIN)",

publisher = "IEEE",

address = "United States",

note = "IEEE International Conference on Industrial Informatics, INDIN ; Conference date: 21-07-2021 Through 23-07-2021",

url = "https://2021.ieee-indin.org/",

}

Shatrov, V & Vyatkin, V 2021, Promela Formal Modelling and Verification of IEC 61499 Systems with comparison to SMV. julkaisussa 2021 IEEE 19th International Conference on Industrial Informatics (INDIN)., 9557513, IEEE, Sivut 1-6, IEEE International Conference on Industrial Informatics, Palma de Mallorca, Espanja, 21/07/2021. https://doi.org/10.1109/INDIN45523.2021.9557513

TY - GEN

T1 - Promela Formal Modelling and Verification of IEC 61499 Systems with comparison to SMV

AU - Shatrov, Viktor

AU - Vyatkin, Valeriy

PY - 2021/10/11

Y1 - 2021/10/11

N2 - This paper presents a method of formal modelling of IEC 61499 systems of Function Blocks with Promela1. The existing method of formal verification of IEC 61499 using SMV (Symbolic Model Verifier) is compared with a new approach of verification using SPIN2 which is an explicit-state model-checker. The performance of both approaches is studied using a set of deterministic systems of multiple computational units as an example and a more complex non-deterministic elevator model.

AB - This paper presents a method of formal modelling of IEC 61499 systems of Function Blocks with Promela1. The existing method of formal verification of IEC 61499 using SMV (Symbolic Model Verifier) is compared with a new approach of verification using SPIN2 which is an explicit-state model-checker. The performance of both approaches is studied using a set of deterministic systems of multiple computational units as an example and a more complex non-deterministic elevator model.

KW - Performance evaluation

KW - Computational modeling

KW - Memory management

KW - XML

KW - Tools

KW - Elevators

KW - IEC Standards

UR - http://www.scopus.com/inward/record.url?scp=85125557282&partnerID=8YFLogxK

U2 - 10.1109/INDIN45523.2021.9557513

DO - 10.1109/INDIN45523.2021.9557513

M3 - Conference article in proceedings

SN - 978-1-7281-4396-5

SP - 1

EP - 6

BT - 2021 IEEE 19th International Conference on Industrial Informatics (INDIN)

PB - IEEE

T2 - IEEE International Conference on Industrial Informatics

Y2 - 21 July 2021 through 23 July 2021

ER -

Promela Formal Modelling and Verification of IEC 61499 Systems with comparison to SMV

Abstrakti

Conference

Pääsy asiakirjaan

Muut tiedostot ja linkit

Sormenjälki

Siteeraa tätä