3 ms·
FM day job: Interpretation of SysML activity diagrams as temporal logic for use with state machine specifications. Module system for state machine with scopin
by johnbender 8mo ago
FM day job:
Interpretation of SysML activity diagrams as temporal logic for use with state machine specifications.
Module system for state machine with scoping, ownership type system and attendant theorems to carry proofs of LTL properties about individual parts forward after composition.
- 4b11b4 8mo agoWait what..? please elaborate or provide any references for further reading!
- johnbender 8mo agoSure! The first is an attempt to provide a semantics for activity diagrams as constraints on a state machine and thereby allow folks to specify correctness properties for the state machine using a visual language. Existing work on semantics for activity diagrams already exists but doesn’t come with tooling in the way that temporal logic does (https://arxiv.org/pdf/1409.2366 https://arxiv.org/pdf/1409.2366) The second is an attempt to fix a long standing problem with state machine specification languages. While many support composition operators (parallel and/or nesting) none of them come with strong theorems about when temporal properties proven about constituent elements will remain valid in the composite.