Design and verification of industrial logic controllers with UML and statecharts

被引：0
|
作者：
Bonfè, M [1 ]
Fantuzzi, C [1 ]
机构：
[1] Univ Ferrara, Dipartimento Ingn, I-44100 Ferrara, Italy
来源：
CCA 2003: PROCEEDINGS OF 2003 IEEE CONFERENCE ON CONTROL APPLICATIONS, VOLS 1 AND 2 | 2003年
关键词：
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
The paper describes a methodological framework that aims to apply formal design and verification techniques to the domain of Logic Control and Supervision for Manufacturing Systems. The methodology is based on a Object-Oriented approach, supported by a syntactical and semantical adaptation of the semiformal software specification languages UML and Statecharts. The modeling languages have been subsequently formalized, according to a semantics that take into account the concepts described in the IEC 61131-3 Standard for industrial controllers programming, in order to prove correctness properties expressed in the temporal logic CTL. The verification process is performed by means of the model checking tool SMV.
引用
收藏
页码：1029 / 1034
页数：6
相关论文
共 50 条
  • [1] Using UML Statecharts with Knowledge Logic Guards
    Drusinsky, Doron
    Shing, Man-Tak
    [J]. MODEL DRIVEN ENGINEERING LANGUAGES AND SYSTEMS, PROCEEDINGS, 2009, 5795 : 586 - 590
  • [2] Transforming UML 'collaborating' statecharts for verification and simulation
    Bobbie, PO
    Ji, YM
    Liang, LS
    [J]. 6TH WORLD MULTICONFERENCE ON SYSTEMICS, CYBERNETICS AND INFORMATICS, VOL XVIII, PROCEEDINGS: INFORMATION SYSTEMS, CONCEPTS AND APPLICATIONS OF SYSTEMICS, CYBERNETICS AND INFORMATICS, 2002, : 61 - 66
  • [3] A case study in verification of UML statecharts: The PROFIsafe protocol
    Malik, R
    Muhlfeld, R
    [J]. JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2003, 9 (02) : 138 - 151
  • [4] Model Checking of UML Activity Diagrams in Logic Controllers Design
    Grobelna, Iwona
    Grobelny, Michal
    Adamski, Marian
    [J]. PROCEEDINGS OF THE NINTH INTERNATIONAL CONFERENCE ON DEPENDABILITY AND COMPLEX SYSTEMS DEPCOS-RELCOMEX, 2014, 286 : 233 - 242
  • [5] Formal verification of UML statecharts with real-time extensions
    David, A
    Möller, MO
    Yi, W
    [J]. FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS, 2002, 2306 : 218 - 232
  • [6] Model Checking in Parallel Logic Controllers Design and Verification
    Doligalski, Michal
    Tkacz, Jacek
    Gratkowski, Tomasz
    [J]. PROCEEDINGS OF THE 2015 FEDERATED CONFERENCE ON SOFTWARE DEVELOPMENT AND OBJECT TECHNOLOGIES, 2017, 511 : 35 - 53
  • [7] Using a process algebra interface for verification and validation of UML statecharts
    Doostali, Saeed
    Babamir, Seyed Morteza
    Javani, Mohammad
    [J]. COMPUTER STANDARDS & INTERFACES, 2023, 86
  • [8] Formal Verification of UML Statecharts using the LOTOS Formal Language
    Javani, Mohamad
    Neysiani, Behzad Soleimani
    Babamir, Seyed Morteza
    [J]. 2015 2ND INTERNATIONAL CONFERENCE ON KNOWLEDGE-BASED ENGINEERING AND INNOVATION (KBEI), 2015, : 754 - 760
  • [9] Design of Reconfigurable Logic Controllers from Hierarchical UML State Machines
    Adamski, Marian
    [J]. ICIEA: 2009 4TH IEEE CONFERENCE ON INDUSTRIAL ELECTRONICS AND APPLICATIONS, VOLS 1-6, 2009, : 82 - +
  • [10] Formal verification and hardware design with statecharts
    Philipps, J
    Scholz, P
    [J]. PROSPECTS FOR HARDWARE FOUNDATIONS: ESPRIT WORKING GROUP 8533 NADA - NEW HARDWARE DESIGN METHODS SURVEY CHAPTERS, 1998, 1546 : 356 - 389
12345