Future Work
We have looked into some formal method tools to generate and automatically verify
embedded system codes. One approach that looked promising is defining specification
with PLC-Automaton -- a subset of duration calculus. This has the benefit that
the system can be implemented with PLCs and codes can be generated
and verified automatically using timed-automata. In the future, we will
look into formal methods for problem specification, implementation and verification.
For the current implementation, we look forward to perform more tests.