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 a day ago | parent [-]

Wait what..? please elaborate or provide any references for further reading!

	▲	johnbender a day ago \| parent [-]
		Sure! 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) 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.