Publication | Closed Access
Modeling and Race Detection of Ladder Diagrams via Ordinary Petri Nets
29
Citations
40
References
2017
Year
Petri NetEngineeringReachability ProblemVerificationComputer-aided VerificationModel CheckingSoftware AnalysisFormal VerificationOrdinary Petri NetSystems EngineeringOrdinary Petri NetsRuntime VerificationStochastic Petri NetComputer EngineeringComputer ScienceRace DetectionReachability AnalysisProgram AnalysisAutomated ReasoningAutomationFormal MethodsLadder DiagramsIndustrial InformaticsPlc ProgramOrdinary Pn
This paper presents an ordinary Petri net (PN)-based approach to the modeling and race-detection problems of programs for programmable logic controllers (PLCs). First, a PLC program is formalized by a graph where nodes represent contacts and coils. Second, an algorithm is proposed to translate this graph into an ordinary PN. Third, a method is presented to detect whether there exists a race in a program by using a reachability graph technique, to locate a race by introducing the race path, and to correct a race by analyzing the subnet that contains it. An example is utilized to illustrate the theoretic results.
| Year | Citations | |
|---|---|---|
Page 1
Page 1