Pith. sign in

REVIEW 3 major objections 5 minor 64 references

Verifying Correctness of PLC Software during System Evolution using Model Containment Approach

T0 review · 3 major / 5 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper claims that a containment checker on Petri nets derived from Sequential Function Charts can soundly verify that an upgraded PLC program preserves every behavior of the original, and that it runs about four times faster than…

desk verdict Plausible SFC regression-checking tool with a real speed claim, but the soundness proof quietly assumes the path-cover completeness that is never proven. read the letter →

arxiv 2509.05596 v1 pith:IZPDZLBT submitted 2025-09-06 cs.SE cs.SC

Soumyadip Bandyopadhyay , Santonu Sarkar This is my paper · ORCID
classification cs.SEcs.SC
keywords PLCsoftwareverificationSequentialFunctionChart(SFC)Petrinetcontainmentsymbolicpathequivalenceexecutioncut-pointsevolutionregressionmodelchecking
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper tries to prove that when PLC software is upgraded, the new version still performs every behavior the old version performed. It translates both versions of a Sequential Function Chart into Petri nets and runs a containment check based on symbolic path equivalence, using execution cut-points that respect PLC tick semantics. If the check succeeds, the old model is contained in the new model, meaning every computation of the old program has an equivalent computation in the upgrade. The paper proves this containment check is sound, meaning it reports no false positives, and measures roughly a fourfold speedup over the verifAPS tool on 80 OSCAT benchmarks. A sympathetic reader cares because regression testing of PLC code is slow and incomplete, and this offers a formal, automated check that a safe upgrade has not silently broken existing functionality.

What carries the argument

The engine is the execution cut-point: a place in the Petri net that is either a static cut-point (initial marking, branch point, back-edge root, or out-port) or is marked during tick-tracking execution when a parallel thread is created. Cut-points split the net into a finite set of paths, and the path cover is the set of all such paths. Containment is checked by comparing each old path against candidate new paths through a normalization step, the WFF constructor, which checks equivalence of the execution-condition formula and the data-transformation expression, with path extension and path merging applied when a candidate path is too short or must be stitched together with converging paths. Tick stamps on the last transitions of matched paths align PLC ticks between the two models.

What would settle it

Construct an original and an upgraded SFC that are behaviorally different only on a second traversal of a loop, for example a guard inside the loop that becomes true only after the first iteration, so that the path cover, which visits each loop exactly once, collapses both iterations into a single path. If the checker reports containment on such a pair, the soundness claim of Theorem 2 is falsified because a computation with different behavior on the second traversal would have been missed.

Watch

Extended reading notes

Core claim

The central claim is Theorem 2: if the containment checker algorithm terminates with the set of unmatched old-model paths, $\Pi_{n,0}$, empty, then the old Petri net model $N_0$ is contained in the new model $N_1$, written $N_0\sqsubseteq N_1$. Containment means that for every out-port $p$ of $N_0$ and every computation $\mu_p$ of $p$, there is a computation $\mu_{p'}$ of the corresponding out-port $p'=f_{\mathrm{out}}(p)$ of $N_1$ such that the two computations have equivalent execution conditions and identical data transformations. The proof works through a path-cover argument: any computation of $N_0$ can be decomposed into a finite sequence of concatenations of parallelizable paths from the constructed path cover, and each such path is matched, possibly after extension or merging, to an equivalent path of $N_1$. The paper also reports that on 80 OSCAT benchmarks the containment check takes 1.43 to 6.12 seconds, about four times faster than verifAPS, and that faulty upgrades are detected with similar speed.

Load-bearing premise

The argument assumes that the set of paths the constructive algorithm generates is a genuine path cover: every computation of the old model can be written as a finite concatenation of parallelizable paths from that set, even though each loop is traversed exactly once and the paper does not prove that the constructive path generation always yields such a cover.

Editorial extensions

If this is right

  • A passing containment check means the upgraded PLC code preserves every old out-port computation, so the preserved portion needs no further regression testing.
  • Because the SFC-to-Petri-net translation is syntactic, the approach extends to any control program that can be mapped to a Petri net, independent of the original PLC language.
  • On the 80 OSCAT benchmarks, containment checking completes in 1.43 to 6.12 seconds, roughly four times faster than verifAPS, and faulty upgrades are detected in similar time.
  • The report generator lists matched and unmatched paths, so a failed check pinpoints concrete places where the upgrade diverges from the original.
  • The tool is sound but not complete: a behavior-preserving but non-bisimilar upgrade may be reported as non-containment, requiring manual review.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A natural next step is to make the path-cover construction itself the object of proof or empirical validation: on small SFCs, one could compare the constructed path cover against the full reachability graph of the Petri net to measure coverage, something the paper does not do.
  • The directionality of containment is well matched to software evolution: an upgrade that only adds new behavior, such as a safety interlock, is contained in the reverse direction, and the tool's asymmetric verdicts correspond to this practical asymmetry.
  • The reported BisimDegree, the ratio of matched paths to total paths, could serve as a regression-risk score for partial upgrades, letting engineers prioritize manual review of unmatched paths rather than discarding the whole verification.
  • The tick-alignment mechanism, devised for PLCs, may transfer to other tick-based reactive languages such as synchronous dataflow languages, where path-based equivalence has not yet been applied.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper proposes a verification approach for PLC software upgrades. SFC programs from an old and a new version are translated into deterministic, 1-safe Petri net models with tick-labeled transitions, and the new model is checked for containment of the old model via symbolic path equivalence. The central theorems (Theorem 1 and Theorem 2) claim that if the algorithm finishes with no unmatched paths in the old model, containment holds. The approach is evaluated on 80 OSCAT-based benchmarks grouped into four classes, with a reported roughly 4x speedup over verifAPS. The paper also reports fault-injection experiments and discusses limitations including non-bisimilar functionally equivalent SFCs and the restriction to traversing loops exactly once.

Significance. If the soundness claim were fully established, the paper would offer a useful, scalable regression-verification tool for a restricted but industrially relevant class of SFC upgrades: the translation to Petri nets is syntactic and simple, the tick-aware execution cut-points are a sensible adaptation to synchronous PLC semantics, and the symbolic path-based checker has the potential to avoid state-space explosion. The 80-benchmark OSCAT evaluation and the explicit comparison with verifAPS are also valuable empirical contributions. However, the significance is conditional: the central soundness theorem rests on an unproved path-cover completeness premise, and the evaluation is reported only as aggregate numbers for four classes without an artifact or per-benchmark data. The paper does not ship machine-checked proofs or reproducible code, and the core path-equivalence machinery is largely imported from the authors' prior work [1,2], which limits independent verification.

major comments (3)
  1. [§5, Theorem 2; Appendix, Algorithms 2-3; Definition 9] The soundness of the containment checker is conditional on an unproved premise: the proof of Theorem 2 in the Appendix begins by asserting 'Let Π0 gives a path cover of N0', but no theorem establishes that the paths generated by Algorithm 3 always form a path cover in the sense of Definition 9 for the supported subclass of SFC-derived Petri nets. Example 2 merely shows insufficiency of static cut-points; Section 7.2 and Section 9 admit that loops are traversed exactly once and that a functionally equivalent but non-bisimilar SFC defeats the path construction. If some reachable computation of an out-port in N0 cannot be expressed as a finite concatenation of parallelizable paths from the generated Π0, then Algorithm 1 can return Πn,0 = ∅ while silently omitting that computation. The reported 'N0 ⊑ N1' would then be a false positive, contradicting the Section 9 claim that the method 'does not give any false positive results.' The authors must either prove path-cover completeness for the supported subclass, or explicitly restrict Theorem 2 and the no-false-positive claim to models for which the generated path set is a complete path cover.
  2. [§5, Algorithm 1 step 8; Definition 10(4)] The treatment of 'uncommon variables' can itself introduce false positives. Step 8 removes all uncommon variables and then computes Rβ and rβ, and Definition 10(4) allows arbitrary association of removed variables with newly introduced variables via ηv. In the running example, the new safety-guard variable S is dropped from the execution condition of path β1·β2, so path equivalence is claimed even though the new guard can, when false, block the old behavior (the robot remains immobilized). No side condition is given to ensure that along every corresponding path the newly introduced guard is always enabled. Without such an invariant, dropping a new guard that affects control flow can make Rα ≡ Rβ even when the old computation has no counterpart in N1. This is a second, independent route to the false positives that Section 9 rules out, and it needs an explicit justification or a restriction on when uncommon-variable elimination is sound.
  3. [§6, Tables 2 and 3] The experimental claims are not supported by the data as reported. Table 2 aggregates results into four classes ('Basic', 'Simple', 'Medium', 'Complex') rather than reporting the 80 individual benchmarks, and it gives no standard deviations, per-benchmark path counts, or timings. The 'nearly 4x' comparison with verifAPS is therefore not substantiated beyond four average points. Table 3 reports a '–' for the Type 2 verifAPS time without explaining whether the tool timed out, crashed, or was not run; this is essential for judging the claim that Type 2 cannot be detected by verifAPS. The paper also provides no artifact, no per-benchmark data, and no independent ground truth for the equivalence labels, making it impossible to check whether the tool's 'yes' and 'no' answers are correct. I recommend providing the benchmark set, the tool, or at least a detailed per-benchmark table with error bars, and a clear protocol for the fault-injection ground truth.
minor comments (5)
  1. [Appendix, Theorem 2 statement] The statement of Theorem 2 in the Appendix is truncated: it reads 'returns Πn,0' with no completion of the condition, while the main-text version is complete. This should be fixed.
  2. [§2 and §4, figure references] Some figure references are inconsistent: Section 2 refers to 'Figure 3(a)' and 'Figure 4(c)' where the surrounding text about the original SFC and its Petri net is not always aligned with the captions, and Section 3 references 'Figure 1' for the functional block diagram that appears as Figure 2.
  3. [§7.2] The sentence 'The method is not scalable at all' is vague and contradicts the scaling claims of Section 6; if the authors mean the method does not scale to non-bisimilar or hierarchical SFCs, that should be stated precisely rather than as a blanket scalability claim.
  4. [Definitions 5-7 and 11] Notation is inconsistent: equivalence of computations is written ≃c, equivalence of models is written ≃ (Definition 7), and path equivalence is written ≃ (Definition 10); the subscripts are dropped in places, making it hard to distinguish computation equivalence from path equivalence. A small notation table would help.
  5. [§4, Definition 2, text after Definition 2] The phrase 'one token corresponds to k variables' in the 1-safe discussion is unclear, and the sentence 'Our Petri net model is deterministic and 1-safe' is asserted without proof; since determinism is used in Definition 4, it should be justified from the SFC translation rules.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; the containment result is a conditional theorem, and the benchmarks are external.

full rationale

I walked the derivation from the SFC-to-Petri-net translation (Section 4.1), through path construction and extension/merging (Algorithms 2-5), to the soundness statements (Theorems 1-2 and their Appendix proofs). The central claim is conditional: Theorem 1 states that if a finite path cover Pi_0 of N_0 (Definition 9) has elementwise equivalent paths in N_1, then N_0 is contained in N_1, and the proof genuinely constructs the required computation in N_1 and checks the successor-marking condition of Definition 3. This is a compositional implication, not an identity by construction: the path-cover hypothesis concerns only N_0, while the conclusion concerns computations in N_1. Theorem 2's proof begins 'Let Pi_0 gives a path cover of N_0', but no lemma proves that Algorithm 3's execution cut-point construction always produces such a path cover for SFC-derived Petri nets, especially under Section 9's 'restriction of traversing each loop exactly once'. That is an unproved soundness/completeness premise and a correctness risk, not a circularity in the sense of a fitted parameter being renamed a prediction or a conclusion being equivalent to its input by construction. The OSCAT evaluation is external, the fault-injection cases are labeled by construction, and the runtime comparisons are measurements rather than derived results. Self-citations [1, 2] supply the path-equivalence vocabulary and prior definitions, but the SFC-to-Petri-net translation, tick-aware execution cut-points, and the containment algorithm are new content; no uniqueness theorem is imported. I therefore find no circular step, while flagging the path-cover completeness gap as the main unverified link in the soundness argument.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The central claim rests on the existence and completeness of a finite path cover for the SFC-derived Petri net model, on the semantic fidelity of the SFC-to-Petri net translation, on the sufficiency of path-based symbolic equivalence for behavior preservation, and on the representativeness of the benchmark selection. No free parameters are fitted. No genuinely new entities are invented, but execution cut-points are a new modeling notion.

assumptions (4)
  • domain assumption Every computation of N0 can be represented as a finite concatenation of parallelizable paths from the constructed path cover (Definition 9).
    Used in the proofs of Theorem 1 and Theorem 2; no proof that the constructive algorithm always produces such a cover.
  • domain assumption The SFC-to-Petri net translation preserves the observable behavior of the SFC program, including tick semantics.
    Section 4.1 states the translation is syntactic and straightforward, but no semantic equivalence proof is given between SFC execution and the generated Petri net model.
  • domain assumption Equivalence of path execution conditions and data transformations over the variables remaining after removing uncommon variables is sufficient for containment of behaviors.
    The definition of path equivalence (Definition 10) and the algorithm's variable-elimination step treat dropped variables as irrelevant to the preserved functionality.
  • domain assumption The OSCAT library programs used as benchmarks are representative of real PLC upgrade scenarios, including the injected faults.
    Section 6.1 selects 80 applications and defines fault types, but no external validation of representativeness is given.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Verifying Correctness of PLC Software during System Evolution using Model Containment Approach." pith.science (2026). https://pith.science/paper/IZPDZLBT

@misc{pith2026250905596,
  author       = {Pith},
  title        = {Pith review of: Verifying Correctness of PLC Software during System Evolution using Model Containment Approach},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/IZPDZLBT}},
  note         = {Machine review of arXiv:2509.05596}
}
read the original abstract

Upgradation of Programmable Logic Controller (PLC) software is quite common to accommodate evolving industrial requirements. Verifying the correctness of such upgrades remains a significant challenge. In this paper, we propose a verification-based approach to ensure the correctness of the existing functionality in the upgraded version of a PLC software. The method converts the older and the newer versions of the sequential function chart (SFC) into two Petri net models. We then verify whether one model is contained within another, based on a novel containment checking algorithm grounded in symbolic path equivalence. For this purpose, we have developed a home-grown Petri net-based containment checker. Experimental evaluation on 80 real-world benchmarks from the OSCAT library highlights the scalability and effectiveness of the framework. We have compared our approach with verifAPS, a popular tool used for software upgradation, and observed nearly 4x performance improvement.

Figures

Figures reproduced from arXiv: 2509.05596 by the authors.

Figure 1
Figure 1. Pick and Place System- original and upgraded version with safety features positive, a fixer combines them, and a second robotic arm deposits the composite item into the green Collect Bin. Conversely, if the parameters fail to meet a positive value, the items are put to the red Waste Bin. The fixing process hinges on intricate calculations adjusting individual scaling factors of items a and b to derive an integrated,… view at source ↗
Figure 2
Figure 2. Functional Block Diagram Path constructor component generates an array of paths derived from a set of cut-points to a cut-point without any intermediary cut-points. The Model Con￾tainment Checker component takes two Petri net models—one for the original SFC code and the other for the updated SFC code—to determine if the up￾dated SFC retains the original SFC’s functionality. This process is referred to as model conta… view at source ↗
Figure 3
Figure 3. Two versions of Pick and Place, (a) Original SFC (b) Upgraded SFC (changes shown in blue color) An SFC code is comparable to a Petri net; formally described in [6]. We reproduce the definition for brevity. Definition 1. A sequential function chart (SFC) S = ⟨S, X, A, TS, s0⟩, is a structure where S is a finite set of steps, X is a finite set of variables, A is a finite set of actions, TS is a finite set of transitio… view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: Two versions of Petri nets [PITH_FULL_IMAGE:figures/full_fig_p006_4.png]
Figure 5
Figure 5. Figure 5: A Petri net model of a computation involving loops path α1, and t8 belongs to α3. As a result, α1, α3 cannot be concatenated in any order. However, if we had p6, p7, p8, p9 and p11 also as cut-points, the path-set would have been α ′ 1 = ⟨{t1}, {t2}, {t4}⟩, α ′ 2 = ⟨{t…
Figure 6
Figure 6. Figure 6: Limitations of our method 7 Discussion In light of the experimental results, we highlight several usage scenarios of the tool and mention a few limitations. 7.1 Utility of the Tool Efficiency in Regression Testing: Since our tool relies on symbolic containment checking…

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

64 extracted references · 63 canonical work pages

  1. [1]

    Equiva- lence checking of petri net models of programs using static and dynamic cut-points

    Soumyadip Bandyopadhyay, Dipankar Sarkar, and Chittaranjan Mandal. Equiva- lence checking of petri net models of programs using static and dynamic cut-points. Acta Informatica, 56(4):321–383, 2019

    work page 2019

  2. [2]

    Mandal, Kunal Banerjee, and Krishnam Raju Duddu

    Soumyadip Bandyopadhyay, Dipankar Sarkar, Chittaranjan A. Mandal, Kunal Banerjee, and Krishnam Raju Duddu. A path construction algorithm for trans- lation validation using PRES+ models.Parallel Process. Lett., 26(2):1650010:1– 1650010:18, 2016

    work page 2016

  3. [3]

    Re- searching evolution in industrial plant automation: Scenarios and documentation of the pick and place unit, 01 2014

    Birgit Vogel-Heuser, Christoph Legat, Jens Folmer, and Stefan Feldmann. Re- searching evolution in industrial plant automation: Scenarios and documentation of the pick and place unit, 01 2014

    work page 2014

  4. [4]

    R. David. Grafcet: a powerful tool for specification of logic controllers.IEEE Transactions on Control Systems Technology, 3(3):253–268, 1995

    work page 1995

  5. [5]

    Proving equivalence between control software variants for pro- grammable logic controllers

    Sebastian Ulewicz, Birgit Vogel-Heuser, Mattias Ulbrich, Alexander Weigl, and Bernhard Beckert. Proving equivalence between control software variants for pro- grammable logic controllers. In20th IEEE Conference on Emerging Technologies & Factory Automation, ETFA 2015, Luxembourg, September 8-11, 2015, pages 1–5. IEEE, 2015

    work page 2015

  6. [6]

    A unifying semantics for sequential function charts

    Nanette Bauer, Ralf Huuck, Ben Lukoschus, and Sebastian Engell. A unifying semantics for sequential function charts. In Hartmut Ehrig, Werner Damm, J¨ org Desel, Martin Große-Rhode, Wolfgang Reif, Eckehard Schnieder, and Engelbert Westk¨ amper, editors,Integration of Software Specification Techniques for Appli- cations in Engineering, Priority Program Sof...

    work page 2004

  7. [7]

    Formal semantics and analysis of multitask PLC ST programs with preemption

    Jaeseo Lee and Kyungmin Bae. Formal semantics and analysis of multitask PLC ST programs with preemption. In Andr´ e Platzer, Kristin Yvonne Rozier, Matteo Pradella, and Matteo Rossi, editors,Formal Methods - 26th International Sympo- sium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part I, volume 14933 ofLecture Notes in Computer Science, p...

    work page 2024

  8. [8]

    Dipankar Sarkar and S. C. De Sarkar. A theorem prover for verifying iterative programs over integers.IEEE Trans. Software Eng., 15(12):1550–1566, 1989

    work page 1989

Show all 64 references
  1. [9]

    Mathematical theory of partial correctness

    Zohar Manna. Mathematical theory of partial correctness. In Erwin Engeler, editor,Symposium on Semantics of Algorithmic Languages, volume 188 ofLecture Notes in Mathematics, pages 252–269. Springer, 1971. 20 Soumyadip Bandyopadhyay and Santonu Sarkar

    1971

  2. [10]

    George C. Necula. Translation validation for an optimizing compiler. InPLDI, pages 83–94, 2000

    2000

  3. [11]

    Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, and Lenore D

    Clark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, and Lenore D. Zuck. Tvoc: A translation validator for optimizing compilers. InCAV, pages 291–295, 2005

    2005

  4. [12]

    Rinard and P

    M. Rinard and P. Diniz. Credible compilation. Technical Report MIT-LCS-TR- 776, MIT, 1999

    1999

  5. [13]

    Wisniewski, I

    R. Wisniewski, I. Grobelna, and A. Karatkevich. Determinism in cyber-physical systems specified by interpreted petri nets.Sensors (Basel), 20(19):5565, Sep 2020

    2020

  6. [14]

    McMillan.Symbolic model checking

    Kenneth L. McMillan.Symbolic model checking. Kluwer, 1993

    1993

  7. [15]

    Regression verification for programmable logic controller software

    Bernhard Beckert, Mattias Ulbrich, Birgit Vogel-Heuser, and Alexander Weigl. Regression verification for programmable logic controller software. In Michael J. Butler, Sylvain Conchon, and Fatiha Za¨ ıdi, editors,Formal Methods and Soft- ware Engineering - 17th International Co...

    2015

  8. [16]

    Lynch, and Eric Feron

    Sayan Mitra, Yong Wang, Nancy A. Lynch, and Eric Feron. Safety verification of model helicopter controller using hybrid input/output automata. In Oded Maler and Amir Pnueli, editors,Hybrid Systems: Computation and Control, 6th Interna- tional Workshop, HSCC 2003 Prague, Czech ...

    2003

  9. [17]

    Modeling and verification of safety-critical sys- tems using safecharts

    Pao-Ann Hsiung and Yen-Hung Lin. Modeling and verification of safety-critical sys- tems using safecharts. InProceedings of the 25th IFIP WG 6.1 International Con- ference on Formal Techniques for Networked and Distributed Systems, FORTE’05, page 290–304, Berlin, Heidelberg, 20...

    2005

  10. [18]

    L. E. Moser and P. M. Melliar-Smith. Formal verification of safety-critical systems. Softw. Pract. Exper., 20(9):799–811, aug 1990

    1990

  11. [19]

    Controller synthesis for linear system with reach-avoid specifications

    Chuchu Fan, Zengyi Qin, Umang Mathur, Qiang Ning, Sayan Mitra, and Mahesh Viswanathan. Controller synthesis for linear system with reach-avoid specifications. IEEE Trans. Autom. Control., 67(4):1713–1727, 2022

    2022

  12. [20]

    Multi-agent safety verification using symmetry transformations

    Hussein Sibai, Navid Mokhlesi, Chuchu Fan, and Sayan Mitra. Multi-agent safety verification using symmetry transformations. In Armin Biere and David Parker, editors,Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, H...

    2020

  13. [21]

    Verification of sequential func- tion charts using smv

    S´ ebastien Bornot, Ralf Huuck, and Ben Lukoschus. Verification of sequential func- tion charts using smv. In Hamid R. Arabnia, editor,Proceedings of the Interna- tional Conference on Parallel and Distributed Processing Techniques and Applica- tions, PDPTA 2000, June 24-29, 20...

    2000

  14. [22]

    Niang, B

    M. Niang, B. Riera, A. Philippot, J. Zaytoon, F. Gellot, and R. Coupat. A method- ology for automatic generation, formal verification and implementation of safe plc programs for power supply equipment of the electric lines of railway control sys- tems.Computers in Industry, 12...

    2020

  15. [23]

    Stefan Klikovits, David P. Y. Lawrence, Manuel Gonzalez-Berges, and Didier Buchs. Automated test case generation for the CTRL programming language using pex: Lessons learned. In Ivica Crnkovic and Elena Troubitsyna, editors,Software PLC Software Verification 21 Engineering for...

    2016

  16. [24]

    An fmi-based initial- ization plugin for INTO-CPS maestro 2

    Simon Thrane Hansen, Casper Thule, and Cl´ audio Gomes. An fmi-based initial- ization plugin for INTO-CPS maestro 2. In Loek Cleophas and Mieke Massink, editors,Software Engineering and Formal Methods. SEFM 2020 Collocated Work- shops - ASYDE, CIFMA, and CoSim-CPS, Amsterdam, ...

    2020

  17. [25]

    Semantic adaptation for FMI co- simulation with hierarchical simulators.Simul., 95(3), 2019

    Cl´ audio Gomes, Bart Meyers, Joachim Denil, Casper Thule, Kenneth Lausdahl, Hans Vangheluwe, and Paul De Meulenaere. Semantic adaptation for FMI co- simulation with hierarchical simulators.Simul., 95(3), 2019

    2019

  18. [26]

    PhD thesis, University of Antwerp, Belgium, 2019

    Cl´ audio Goncalves Gomes.Property preservation in co-simulation. PhD thesis, University of Antwerp, Belgium, 2019

    2019

  19. [27]

    Springer Berlin Heidelberg, Berlin, Heidelberg, 2004

    Nanette Bauer, Sebastian Engell, Ralf Huuck, Sven Lohmann, Ben Lukoschus, Manuel Remelhe, and Olaf Stursberg.Verification of PLC Programs Given as Sequential Function Charts, pages 517–540. Springer Berlin Heidelberg, Berlin, Heidelberg, 2004

    2004

  20. [28]

    Modeling error propagation in a modular plant

    Santonu Sarkar, Nicolai Schoch, and Mario Hoernicke. Modeling error propagation in a modular plant. In27th IEEE International Conference on Emerging Tech- nologies and Factory Automation, ETFA 2022, Stuttgart, Germany, September 6-9, 2022, pages 1–4. IEEE, 2022

    2022

  21. [29]

    Rossi, Jean-Jacques Lesage, and Jean-Marc Roussel

    O. Rossi, Jean-Jacques Lesage, and Jean-Marc Roussel. Formal validation of plc programs: A survey.European Control Conference, ECC 1999 - Conference Pro- ceedings, 01 1999

    1999

  22. [30]

    Automatic test case generation for plc pro- grams using coverage metrics.2015 IEEE 20th Conference on Emerging Technolo- gies & Factory Automation (ETFA), pages 1–4, 2015

    Hendrik Simon, Nico Friedrich, Sebastian Biallas, Stefan Hauck-Stattelmann, Bas- tian Schlich, and Stefan Kowalewski. Automatic test case generation for plc pro- grams using coverage metrics.2015 IEEE 20th Conference on Emerging Technolo- gies & Factory Automation (ETFA), page...

    2015

  23. [31]

    B S I Standards, 2002

    British Standards Institute Staff.GRAFCET Specification Language for Sequential Function Charts. B S I Standards, 2002

    2002

  24. [32]

    Tournier, B

    J-C. Tournier, B. Fern´ andez Adiego, and I.D. Lopez-Miguel. PLCverif: Sta- tus of a Formal Verification Tool for Programmable Logic Controller. In Proc. ICALEPCS’21, number 18 in International Conference on Accelerator and Large Experimental Physics Control Systems, pages 248...

    2022

  25. [33]

    Model-based verification of plc programs using simulink design

    Nannan He, Victor Oke, and Gale Allen. Model-based verification of plc programs using simulink design. In2016 IEEE International Conference on Electro Infor- mation Technology (EIT), pages 0211–0216, 2016

    2016

  26. [34]

    Cooperative verification of plc programs using coveriteam: Towards a reliable and secure industrial control systems

    Chibuzo Ukegbu and Hoda Mehrpouyan. Cooperative verification of plc programs using coveriteam: Towards a reliable and secure industrial control systems. In Proceedings of Cyber-Physical Systems and Internet of Things Week 2023, CPS- IoT Week ’23, page 37–42, New York, NY, USA,...

    2023

  27. [35]

    Filkorn, M

    Th. Filkorn, M. H¨ olzlein, P. Warkentin, and M. Weiβ. Formal verification of plc- programs.IFAC Proceedings Volumes, 32(2):1513–1518, 1999. 14th IFAC World Congress 1999, Beijing, Chia, 5-9 July

    1999

  28. [36]

    Combinational model- checking of plc programs’ verification based on instructions

    Litian Xiao, Mengyuan Li, Ming Gu, and Jiaguang Sun. Combinational model- checking of plc programs’ verification based on instructions. In2014 IEEE Inter- national Conference on Mechatronics and Automation, pages 1335–1340, 2014. 22 Soumyadip Bandyopadhyay and Santonu Sarkar

    2014

  29. [37]

    An overview of model checking practices on verification of plc software.Softw

    Tolga Ovatman, Atakan Aral, Davut Polat, and Ali Osman ¨Unver. An overview of model checking practices on verification of plc software.Softw. Syst. Model., 15(4):937–960, October 2016

    2016

  30. [38]

    Work in progress - model-check PLC programs: Towards a efficient formalization ap- proach

    Jessica Ravakambinintsoa, Emil Dumitrescu, Eric Zama¨ ı, and Denis Chalon. Work in progress - model-check PLC programs: Towards a efficient formalization ap- proach. In29th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2024, Padova, Italy,...

    2024

  31. [39]

    Safe programming of plc using formal verification methods

    Olivier De Smet, Sandrine Couffin, Olivier Rossi, G´ eraud Canet, Jean-Jacques Lesage, Philippe Schnoebelen, and H´ el` ene Papini. Safe programming of plc using formal verification methods. 2007

    2007

  32. [40]

    Cooperative verification of PLC programs using coveriteam: Towards a reliable and secure industrial control systems

    Chibuzo Ukegbu and Hoda Mehrpouyan. Cooperative verification of PLC programs using coveriteam: Towards a reliable and secure industrial control systems. In Proceedings of Cyber-Physical Systems and Internet of Things Week 2023, CPS- IoT Week 2023 Workshops, San Antonio, TX, US...

    2023

  33. [41]

    Generalised test tables: A practical specification language for reactive systems

    Bernhard Beckert, Suhyun Cha, Mattias Ulbrich, Birgit Vogel-Heuser, and Alexan- der Weigl. Generalised test tables: A practical specification language for reactive systems. In Nadia Polikarpova and Steve A. Schneider, editors,Integrated Formal Methods - 13th International Conf...

    2017

  34. [42]

    A tool for the certification of plcs based on a coq semantics for sequential function charts.CoRR, abs/1102.3529, 2011

    Jan Olaf Blech. A tool for the certification of plcs based on a coq semantics for sequential function charts.CoRR, abs/1102.3529, 2011

    2011 arXiv

  35. [43]

    Verification of PLC properties based on formal semantics in coq

    Jan Olaf Blech and Sidi Ould Biha. Verification of PLC properties based on formal semantics in coq. In Gilles Barthe, Alberto Pardo, and Gerardo Schneider, editors, Software Engineering and Formal Methods - 9th International Conference, SEFM 2011, Montevideo, Uruguay, November...

    2011

  36. [44]

    On formal reasoning on the semantics of PLC using coq.CoRR, abs/1301.3047, 2013

    Jan Olaf Blech and Sidi Ould Biha. On formal reasoning on the semantics of PLC using coq.CoRR, abs/1301.3047, 2013

    2013 arXiv

  37. [45]

    Springer US, Boston, MA, 2000

    S´ ebastien Bornot, Ralf Huuck, Yassine Lakhnech, and Ben Lukoschus.An Abstract Model for Sequential Function Charts, pages 255–264. Springer US, Boston, MA, 2000

    2000

  38. [46]

    Equivalence checking of static affine programs using widening to handle recurrences

    Sven Verdoolaege, Gerda Janssens, and Maurice Bruynooghe. Equivalence checking of static affine programs using widening to handle recurrences. InProceedings of CAV ’09, pages 599–613, 2009

    2009

  39. [47]

    Black-box equivalence checking across compiler optimizations

    Manjeet Dahiya and Sorav Bansal. Black-box equivalence checking across compiler optimizations. In Bor-Yuh Evan Chang, editor,APLAS 2017, Suzhou, China, November 27-29, 2017, Proceedings, volume 10695 ofLecture Notes in Computer Science, pages 127–147. Springer, 2017

    2017

  40. [48]

    Automatic generation of debug headers through blackbox equiva- lence checking

    Vaibhav Kiran Kurhe, Pratik Karia, Shubhani Gupta, Abhishek Rose, and So- rav Bansal. Automatic generation of debug headers through blackbox equiva- lence checking. In Jae W. Lee, Sebastian Hack, and Tatiana Shpeisman, edi- tors,IEEE/ACM International Symposium on Code Generat...

    2022

  41. [49]

    Validating high-level synthesis

    Sudipta Kundu, Sorin Lerner, and Rajesh Gupta. Validating high-level synthesis. In Aarti Gupta and Sharad Malik, editors,Computer Aided Verification, 20th In- ternational Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceed- ings, volume 5123 ofLecture Notes in C...

    2008

  42. [50]

    Sudipta Kundu, Sorin Lerner, and Rajesh K. Gupta. Translation validation of high-level synthesis.IEEE Trans. on CAD of Integrated Circuits and Systems, 29(4):566–579, 2010

    2010

  43. [51]

    Ardiff: scaling program equivalence checking via iterative abstraction and refinement of common code

    Sahar Badihi, Faridah Akinotcho, Yi Li, and Julia Rubin. Ardiff: scaling program equivalence checking via iterative abstraction and refinement of common code. InProceedings of the 28th ACM Joint Meeting on European Software Engineer- ing Conference and Symposium on the Foundat...

    2020

  44. [52]

    Semantic code refactoring for abstract data types.Proc

    Shankara Pailoor, Yuepeng Wang, and I¸ sıl Dillig. Semantic code refactoring for abstract data types.Proc. ACM Program. Lang., 8(POPL), January 2024

    2024

  45. [53]

    Data-driven equivalence checking.SIGPLAN Not., 48(10):391–406, October 2013

    Rahul Sharma, Eric Schkufza, Berkeley Churchill, and Alex Aiken. Data-driven equivalence checking.SIGPLAN Not., 48(10):391–406, October 2013

    2013

  46. [54]

    Effective use of smt solvers for program equivalence checking through invariant-sketching and query-decomposition

    Shubhani Gupta, Aseem Saxena, Anmol Mahajan, and Sorav Bansal. Effective use of smt solvers for program equivalence checking through invariant-sketching and query-decomposition. InTheory and Applications of Satisfiability Testing – SAT 2018: 21st International Conference, SAT ...

    2018

  47. [55]

    Client-specific equivalence checking

    Federico Mora, Yi Li, Julia Rubin, and Marsha Chechik. Client-specific equivalence checking. InProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE ’18, page 441–451, New York, NY, USA,

  48. [56]

    Semantic pro- gram alignment for equivalence checking

    Berkeley Churchill, Oded Padon, Rahul Sharma, and Alex Aiken. Semantic pro- gram alignment for equivalence checking. InProceedings of the 40th ACM SIG- PLAN Conference on Programming Language Design and Implementation, PLDI 2019, page 1027–1040, New York, NY, USA, 2019. Associ...

    2019

  49. [57]

    Eqbench: A dataset of equivalent and non- equivalent program pairs

    Sahar Badihi, Yi Li, and Julia Rubin. Eqbench: A dataset of equivalent and non- equivalent program pairs. In2021 IEEE/ACM 18th International Conference on Mining Software Repositories (MSR), pages 610–614, 2021

    2021

  50. [58]

    Verification of behavioural elements of uml models using b

    Ninh-Thuan Truong and Jeanine Souquieres. Verification of behavioural elements of uml models using b. InProceedings of the 2005 ACM Symposium on Applied Computing, SAC ’05, page 1546–1552, New York, NY, USA, 2005. Association for Computing Machinery

    2005

  51. [59]

    Con- sistency in UML and B multi-view specifications

    Dieu Donn´ e Okalas Ossami, Jean-Pierre Jacquot, and Jeanine Souqui` eres. Con- sistency in UML and B multi-view specifications. In Judi Romijn, Graeme Smith, and Jaco van de Pol, editors,Integrated Formal Methods, 5th International Confer- ence, IFM 2005, Eindhoven, The Nethe...

    2005

  52. [60]

    Towards the formal verification of sysml v2 models

    Vince Moln´ ar, Bence Graics, Andr´ as V¨ or¨ os, Stefano Tonetta, Luca Cristoforetti, Greg Kimberly, Pamela Dyer, Kristin Giammarco, Manfred Koethe, John Hester, Jamie Smith, and Christoph Grimm. Towards the formal verification of sysml v2 models. InProceedings of the ACM/IEE...

    2024

  53. [61]

    Hardware behavioural modelling, verification and synthesis with uml 2.x activity diagrams.IFAC Pro- ceedings Volumes, 45(7):134–139, 2012

    Michal Grobelny, Iwona Grobelna, and Marian Adamski. Hardware behavioural modelling, verification and synthesis with uml 2.x activity diagrams.IFAC Pro- ceedings Volumes, 45(7):134–139, 2012. 11th IFAC,IEEE International Conference on Programmable Devices and Embedded Systems....

    2012

  54. [62]

    Integration of modeling and verification for system model based on karma language

    Jie Ding, Michel Reniers, Jinzhi Lu, Guoxin Wang, Lei Feng, and Dimitris Kiritsis. Integration of modeling and verification for system model based on karma language. InProceedings of the 18th ACM SIGPLAN International Workshop on Domain- Specific Modeling, DSM 2021, page 41–50...

    2021

  55. [63]

    Verification of nonblocking- ness in bounded petri nets with a semi-structural approach

    Chao Gu, Ziyue Ma, Zhiwu Li, and Alessandro Giua. Verification of nonblocking- ness in bounded petri nets with a semi-structural approach. In2019 IEEE 58th Conference on Decision and Control (CDC), pages 6718–6723, 2019. PLC Software Verification 25 Appendix Algorithm 2:PathCo...

    2019

  56. [2018]

    Association for Computing Machinery

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.