Demonstrators


 

Automated software synthesis for modular production systems


FESTO demonstrator with automatic occupancy check, face detection with error handling, and object storing by color. The executable code is first by synthesizing the PDDL FESTO model, followed by using a script to automatically translate each atomic action to corresponding hardware control actions. Details can be found in MGSyn

 

Automatic software synthesis of PLC controllers


Execute the automatically synthesized controller program on CODESYS soft PLC. Details can be found in G4LTL-ST

Formal verification of neural networks


Perform formal verification to find adversarial images, and to formally secure highway motion predictors. Details can be found in our ATVA'17 paper

Formal synthesis of Lustre programs for safety critical systems


Use autoCode4 to synthesize actor-based controllers from formal specification represented in linear temporal logic. The working environment is Ptolemy II, an open-source tool for engineering cyber-physical systems. 


 
http://www6.in.tum.de/~chengch/vissbip/
Use distributed priority synthesis to automatically create distributed controllers such that undesired behavior can not occur (click on the figure to enlarge). Details can be found in VissBIP 


ą
Chih-Hong Cheng,
Oct 6, 2015, 7:32 AM
Comments