Updating the initial page to include information about both tools

lagarcia38 · Apr 19, 2019 · f678797 · f678797
1 parent 8f6a04e
commit f678797
Show file tree

Hide file tree

Showing 18 changed files with 28 additions and 364 deletions.
diff --git a/README.md b/README.md
@@ -1,18 +1,11 @@
-# HyPLC: Hybrid Programmable Logic Controller Program Translation for Verification
+# HyPLC: Hybrid Programmable Logic Controller Program Translation for Verification[1]
+Programmable Logic Controllers (PLCs) provide a prominent choice of implementation platform for safety-critical industrial control systems. Formal verification provides ways of establishing correctness guarantees, which can be quite important for such safety-critical applications. But since PLC code does not include an analytic model of the system plant, their verification is limited to discrete properties. In this paper, we, thus, start the other way around with hybrid programs that include continuous plant models in addition to discrete control algorithms. Even deep correctness properties of hybrid programs can be formally verified in the theorem prover KeYmaera X that implements differential dynamic logic, dL, for hybrid programs. After verifying the hybrid program, we now present an approach for translating hybrid programs into PLC code. The new tool, **HyPLC**, implements this translation of discrete control code of verified hybrid program models to PLC controller code and, vice versa, the translation of existing PLC code into the discrete control actions for a hybrid program given an additional input of the continuous dynamics of the system to be verified. This approach allows for the generation of real controller code while preserving, by compilation, the correctness of a valid and verified hybrid program. PLCs are common cyber-physical interfaces for safety-critical industrial control applications, and HyPLC serves as a pragmatic tool for bridging formal verification of complex cyber-physical systems at the algorithmic level of hybrid programs with the execution layer of concrete PLC implementations.
 
-Structured Text to Hybrid Program Translation
-============
-This is the half of the HyPLC tool that translates the IEC61131-3 standard structured text programming language for PLCs to a hybrid program specified in differential dynamic logic. This makes up one half of the HyPLC tool presented in [1]. For the converse translation, please visit the project link page. The tool has been directly integrated into the KeYmaera X command-line tool.
-*README TODO: Add usage examples 
-##### Usage
-You can use the hyplc-st-to-hp.py script to perform the translation for a given st file as follows:
-* python3 ./hyplc-st-to-hp.py st-file [hp-file]
-where <st-file> is a structured text program file that conforms to the subset of the IEC61131-3 standard defined in our paper, and <hp-file> is an option for providing a hybrid program where the ctrl can be replaced. This can be done by essentially writing a hybrid program as usual and including a placeholder "ctrl" variable where the  ctrl of the system should reside.
+![HyPLC System Overview](./docs/figures/hyplc-overview.jpg)
 
+##### Usage
+Each translation direction has its own implementation. For the translation of structured text to hybrid programs, please visit the **hyplc-st-to-hp** directory. For the details about the hybrid program to structured text translation implementation, please see the details in the **hyplc-hp-to-st** directory.
 
-Installation
-============
-This project depends on ANTLR4 version 4.7.1 as well as Python3. Please note that ANTLR4 is very version-dependent.
 
 Publications
 ============

diff --git a/hyplc-hp-to-st/README.md b/hyplc-hp-to-st/README.md
@@ -0,0 +1,11 @@
+# Hybrid Program to Structured Text Translation
+============
+This repo simply is a placeholder until we integrate the the HP to ST command line option into the Github repo. Right now, the jar file in this repo is a runnable verasion of KeYmaera X that has the associated command line option (see STL).  The tool takes as input the hybrid program in scan cycle normal form and generates a structured text program that preserves the semantics as well as any safety guarantees.
+
+
+##### Usage
+You can refer to the command line KeYmaera X  usage information from the [KeYmaera X repo page.](https://github.com/LS-Lab/KeYmaeraX-release). The input will be a kyx file and hte output will
+
+java -jar ./keymaerax.jar -genSTFile <model-file.kyx> -out file.st
+
+The out file will be a structured text program.
diff --git a/parser/IECSTExpressions.py → hyplc-st-to-hp/IECSTExpressions.py b/parser/IECSTExpressions.py → hyplc-st-to-hp/IECSTExpressions.py
diff --git a/parser/IECSTGrammar.g4 → hyplc-st-to-hp/IECSTGrammar.g4 b/parser/IECSTGrammar.g4 → hyplc-st-to-hp/IECSTGrammar.g4
diff --git a/parser/IECSTGrammar.interp → hyplc-st-to-hp/IECSTGrammar.interp b/parser/IECSTGrammar.interp → hyplc-st-to-hp/IECSTGrammar.interp
diff --git a/parser/IECSTGrammar.tokens → hyplc-st-to-hp/IECSTGrammar.tokens b/parser/IECSTGrammar.tokens → hyplc-st-to-hp/IECSTGrammar.tokens
diff --git a/parser/IECSTGrammarLexer.interp → hyplc-st-to-hp/IECSTGrammarLexer.interp b/parser/IECSTGrammarLexer.interp → hyplc-st-to-hp/IECSTGrammarLexer.interp
diff --git a/parser/IECSTGrammarLexer.py → hyplc-st-to-hp/IECSTGrammarLexer.py b/parser/IECSTGrammarLexer.py → hyplc-st-to-hp/IECSTGrammarLexer.py
diff --git a/parser/IECSTGrammarLexer.tokens → hyplc-st-to-hp/IECSTGrammarLexer.tokens b/parser/IECSTGrammarLexer.tokens → hyplc-st-to-hp/IECSTGrammarLexer.tokens
diff --git a/parser/IECSTGrammarParser.py → hyplc-st-to-hp/IECSTGrammarParser.py b/parser/IECSTGrammarParser.py → hyplc-st-to-hp/IECSTGrammarParser.py
diff --git a/parser/IECSTGrammarVisitor.py → hyplc-st-to-hp/IECSTGrammarVisitor.py b/parser/IECSTGrammarVisitor.py → hyplc-st-to-hp/IECSTGrammarVisitor.py
diff --git a/parser/IECSTtoHPPrettyPrinter.py → hyplc-st-to-hp/IECSTtoHPPrettyPrinter.py b/parser/IECSTtoHPPrettyPrinter.py → hyplc-st-to-hp/IECSTtoHPPrettyPrinter.py
diff --git a/hyplc-st-to-hp/README.md b/hyplc-st-to-hp/README.md
@@ -0,0 +1,12 @@
+# Structured Text to Hybrid Program Translation
+============
+This is the half of the HyPLC tool that translates the IEC61131-3 standard structured text programming language for PLCs to a hybrid program specified in differential dynamic logic. This makes up one half of the HyPLC tool presented in [1]. For the converse translation, please visit the project link page. The tool has been directly integrated into the KeYmaera X command-line tool.
+*README TODO: Add usage examples 
+##### Usage
+You can use the hyplc-st-to-hp.py script to perform the translation for a given st file as follows:
+</br>
+* python3 ./hyplc-st-to-hp.py st-file [hp-file]
+
+where <st-file> is a structured text program file that conforms to the subset of the IEC61131-3 standard defined in our paper, and <hp-file> is an option for providing a hybrid program where the ctrl can be replaced. This can be done by essentially writing a hybrid program as usual and including a placeholder "ctrl" variable where the  ctrl of the system should reside.
+
+
diff --git a/parser/examples/SWaT-P1-T1-model-before.kyx → ...o-hp/examples/SWaT-P1-T1-model-before.kyx b/parser/examples/SWaT-P1-T1-model-before.kyx → ...o-hp/examples/SWaT-P1-T1-model-before.kyx
diff --git a/...er/examples/SWaT-P1-T1-model-expected.kyx → ...hp/examples/SWaT-P1-T1-model-expected.kyx b/...er/examples/SWaT-P1-T1-model-expected.kyx → ...hp/examples/SWaT-P1-T1-model-expected.kyx
diff --git a/parser/examples/water-treatment-proc-1.st → ...-to-hp/examples/water-treatment-proc-1.st b/parser/examples/water-treatment-proc-1.st → ...-to-hp/examples/water-treatment-proc-1.st
diff --git a/parser/hyplc-st-to-hp.py → hyplc-st-to-hp/hyplc-st-to-hp.py b/parser/hyplc-st-to-hp.py → hyplc-st-to-hp/hyplc-st-to-hp.py