ﻻ يوجد ملخص باللغة العربية
Ladder Logics is a programming language standardized in IEC 61131-3 and widely used for programming industrial Programmable Logic Controllers (PLC). A PLC program consists of inputs (whose values are given at runtime by factory sensors), outputs (whose values are given at runtime to factory actuators), and the logical expressions computing output values from input values. Due to the graphical form of Ladder programs, and the amount of inputs and outputs in typical industrial programs, debugging such programs is time-consuming and error-prone. We present, in this paper, a Why3-based tool prototype we have implemented for automating the use of deductive verification in order to provide an easy-to-use and robust debugging tool for Ladder programmers.
Software engineering of modular robotic systems is a challenging task, however, verifying that the developed components all behave as they should individually and as a whole presents its own unique set of challenges. In particular, distinct component
Among formal methods, the deductive verification approach allows establishing the strongest possible formal guarantees on critical software. The downside is the cost in terms of human effort required to design adequate formal specifications and to su
Applying program analyses to Software Product Lines (SPLs) has been a fundamental research problem at the intersection of Product Line Engineering and software analysis. Different attempts have been made to lift particular product-level analyses to r
This volume contains the proceedings of F-IDE 2019, the fifth international workshop on Formal Integrated Development Environment, which was held on October 7, 2019 in Porto, Portugal, as part of FM19, the 3rd World Congress on Formal Methods. High l
This volume contains the proceedings of F-IDE 2021, the sixth international workshop on Formal Integrated Development Environment, which was held online on May 24-25, 2021, as part of NFM21, the 13th NASA Formal Methods Symposium. High levels of safe