Modelling, Specifying, and Verifying Real-Time Embedded Computer Systems. - Jonathan S. Ostroff; Walter Murray Wonham (RTSS, 1987)

Automated Verification of Timed Transition Models. - Jonathan S. Ostroff (Automatic Verification Methods for Finite State Systems, 1989)

Verifying finite state real-time discrete event processes. - Jonathan S. Ostroff (ICDCS, 1989)

Real-Time Temporal Logic Decision Procedures. - Jonathan S. Ostroff (RTSS, 1989)

Mechanizing the verification of real-time discrete systems. - Jonathan S. Ostroff (Microprocessing and Microprogramming, 1989)

Deciding Properties of Timed Transition Models. - Jonathan S. Ostroff (IEEE Trans. Parallel Distributed Syst., 1990)

Verification of Safety Critical Systems Using TTM/RTTL. - Jonathan S. Ostroff (REX Workshop, 1991)

Constraint Logic Programming for Reasoning About Discrete Event Processes. - Jonathan S. Ostroff (J. Log. Program., 1991)

Formal methods for the specification and design of real-time safety critical systems. - Jonathan S. Ostroff (J. Syst. Softw., 1992)

A Verifier for Real-Time Properties. - Jonathan S. Ostroff (Real Time Syst., 1992)

Automated modular specification and verification of real-time reactive systems. - Jonathan S. Ostroff (WIFT, 1995)

Model Reduction of Modules for State-Even Temporal Logics. - Mark Lawford; Jonathan S. Ostroff; Walter Murray Wonham (FORTE, 1996)

A visual toolset for the design of real-time discrete-event systems. - Jonathan S. Ostroff (IEEE Trans. Control. Syst. Technol., 1997)

From Z to BON/Eiffel. - Richard F. Paige; Jonathan S. Ostroff (ASE, 1998)

Developing BON as an Industrial-Strength Formal Method. - Richard F. Paige; Jonathan S. Ostroff (World Congress on Formal Methods, 1999)

A Comparison of the Business Object Notation and the Unified Modelling Language. - Richard F. Paige; Jonathan S. Ostroff (UML, 1999)

Composition and Refinement of Discrte Real-Time Systems. - Jonathan S. Ostroff (ACM Trans. Softw. Eng. Methodol., 1999)

Discussion on: 'A Contribution to the Validation of Grafcet Controlled Systems' by J. Zaytoon. - Jonathan S. Ostroff; H. Alla; Karl-Erik Årzén; Janan Zaytoon (Eur. J. Control, 2000)

The logic of software design. - Jonathan S. Ostroff; Richard F. Paige (IEE Proc. Softw., 2000)

Principles for modeling language design. - Richard F. Paige; Jonathan S. Ostroff; Phillip J. Brooke (Inf. Softw. Technol., 2000)

Metamodelling and Conformance Checking with PVS. - Richard F. Paige; Jonathan S. Ostroff (FASE, 2001)

A Proposal for a Lightweight Rigorous UML-Based Development Method for Reliable Systems. - Richard F. Paige; Jonathan S. Ostroff (pUML, 2001)

BON-CASE: An Extensible CASE Tool for Formal Specification and Reasoning. - Richard F. Paige; Liliya Kaminskaya; Jonathan S. Ostroff; Jason Lancaric (J. Object Technol., 2002)

The Single Model Principle. - Richard F. Paige; Jonathan S. Ostroff (J. Object Technol., 2002)

BON development tool. - Ali Taleghani; Jonathan S. Ostroff (eTX, 2003)

Theorem Proving Support for View Consistency Checking. - Richard F. Paige; Jonathan S. Ostroff; Phillip J. Brooke (Obj. Logiciel Base données Réseaux, 2003)

Specification-Driven Design with Eiffel and Agents for Teaching Lightweight Formal Methods. - Richard F. Paige; Jonathan S. Ostroff (TFM, 2004)

Agile Specification-Driven Development. - Jonathan S. Ostroff; David Makalsky; Richard F. Paige (XP, 2004)

ERC - An object-oriented refinement calculus for Eiffel. - Richard F. Paige; Jonathan S. Ostroff (Formal Aspects Comput., 2004)

SECG: The SCOOP-to-Eiffel Code Generator. - Oleksandr Fuks; Jonathan S. Ostroff; Richard F. Paige (J. Object Technol., 2004)

E-Tester: a Contract-Aware and Agent-Based Unit Testing Framework for Eiffel. - Jonathan S. Ostroff; Richard F. Paige; David Makalsky; Phillip J. Brooke (J. Object Technol., 2005)

Testable Requirements and Specifications. - Jonathan S. Ostroff; Faraz Ahmadi Torshizi (TAP, 2007)

Metamodel-based model conformance and multiview consistency checking. - Richard F. Paige; Phillip J. Brooke; Jonathan S. Ostroff (ACM Trans. Softw. Eng. Methodol., 2007)

The SCOOP Concurrency Model in Java-like Languages. - Faraz Ahmadi Torshizi; Jonathan S. Ostroff; Richard F. Paige; Marsha Chechik (CPA, 2009)

Contracts for concurrency. - Piotr Nienaltowski; Bertrand Meyer 001; Jonathan S. Ostroff (Formal Aspects Comput., 2009)

Beyond contracts for concurrency. - Jonathan S. Ostroff; Faraz Ahmadi Torshizi; Hai Feng Huang; Bernd Schoeller (Formal Aspects Comput., 2009)

TTM/PAT: Specifying and Verifying Timed Transition Models. - Jonathan S. Ostroff; Chen-Wei Wang; Simon Hudon; Yang Liu 003; Jun Sun 001 (FTSCS, 2013)

Precise Documentation and Validation of Requirements. - Chen-Wei Wang; Jonathan S. Ostroff; Simon Hudon (FTSCS, 2013)

Using Indexed and Synchronous Events to Model and Validate Cyber-Physical Systems. - Chen-Wei Wang; Jonathan S. Ostroff; Simon Hudon (ESSS, 2015)

The Unit-B method: refinement guided by progress concerns. - Simon Hudon; Thai Son Hoang; Jonathan S. Ostroff (Softw. Syst. Model., 2016)

Modelling and Testing Requirements via Executable Abstract State Machines. - Jonathan S. Ostroff; Chen-Wei Wang (MoDRE@RE, 2018)