Integrity Constraints for Microcontroller Programming in Datalog

This is a small proof-of-concept implementation of the constraint check in the submitted paper "Integrity Constraints for Microcontroller Programming in Datalog".

• src.zip (Prolog Program Code, Last Update: March 29, 2021)
• blink0.mlg (Example Input File)
• paper.pdf (Paper in Preparation: Integrity Constraints for Microcontroller Programming in Datalog)

The program is being actively developed. Please check again this webpage in a few days. There also will be more examples soon. And a specification of the input syntax. The parser could also check for more errors.

Datalog for Arduino:

More work on Datalog for Arduino and the Lego EV3 Roboter System is reported at:

https://dbs.informatik.uni-halle.de/microlog/

(Currently, the language of this main project, which contains a compiler from Datalog to Arduino C code, differs in some slight details.)

README:

• The prototype is a Prolog program (tested with SWI Prolog). If you do not have Prolog yet, download SWI Prolog from:

  https://www.swi-prolog.org/.

  If you have another Prolog system, and my program should not work with that, please let me know: brass@informatik.uni-halle.de. I am interested in portable programming.
• Start the Prolog system, and load ("consult") this program. If file 'ctest.pl' is in the same directory:

  ?- [ctest].

  (here, ?- is the prompt of the Prolog system). Do not forget the full stop '.' at the end of the command. Since ctest.pl loads the other Prolog source files, the current directory should be the src directory.
• If you just want to run the example from the paper:

  ?- example.

  This uses a built-in version of the example rules and constraints.
• You can also load the example from the file blink0.mlg. This is done with

  ?- load(blink0).

  You can also specify the full path, if necessary:

  ?- load('C:/my/path/blink0.mlg').

  To see the loaded rules and constraints (already transformed to pure Datalog), use

  ?- show.

  To check whether the constraints are guaranteed to hold:

  ?- ctest.

• The currently available user commands (Prolog predicates) are listed with:

  ?- h.

  There are a few options that can be set, but they are mainly for debugging the program. All options are listed with:

  ?- show_opt.

• The classic way to leave a Prolog system is

  ?- halt.

  (Again, the full stop at the end is important in Prolog.) I also defined a predicate quit that does the same.
• The program will be developed further. Please check for new versions at:

  http://users.informatik.uni-halle.de/~brass/micrologS/

  The current version is 0.4 from March 29, 2021.
• This version has a small self-built consistency check for the arithmetic constraints. It is probably not complete, however this is sufficient for the correctness of the approach: If the prover can show all violation conditions as inconsistent, the constraints/invariants are guaranteed to be satisfied. We will continue to work on this, but at the moment it seems more interesting to add further techniques for showing that no actually occurring model satisfies a violation condition. It is possible that violation conditions are formally satisfiable, but the corresponding models do not occur in the iteration for computing the minimal model, and therefore the constraints are actually satisfied. Currently, we are trying to precompute information about occurring states and state transitions.

Source Code:

You can download a zip-archive of all source files.

• ctest.pl: Main program.
• examples.pl: Data of the Examples.
• util.pl: Some General Utility Predicates (lists, file interface).
• opt.pl: Management of Options.
• types.pl: Data structure definitions (is_T, print_T and more).
• input.pl: Input Data, Parsing, Preprocessing.
• sld.pl: SLD Resolution Steps, Computation of Violation Conditions.
• prover.pl: Prover (Consistency Checker for Built-In Predicates).