These are located in the "Deliverables" page above.
They are the result of a one year effort to analyse the numerous artifacts produced by Blue Ortho during the development of its ExactechGPS-TKA Medical Cyber-Physical System: design documents, surgery reports, execution traces, QMS procedures, unit tests, source code trace points, etc.
The WP6/D1 Technical Report analyses a variety of MCPS requirements and explores whether and how they can be formalized as properties of execution traces. The report introduces seemingly important differences between “Assumed properties”, “Required properties” and “Usage properties” and draws partial conclusions on further MODMED research.
Built upon WP6/D1, the WP1/D1 Preliminary Definition of MODMED DSL describes the syntax and formal semantics of a language for property specification on execution traces. This DSL strives to be practical by combining high expressiveness and ease of use.