Home

Publications

ShortCV

York University

York Library

CS@York

Techreports
  1. Jonathan S. Ostroff and Chen-Wei Wang, "Modelling and Testing Requirements via Executable Abstract State Machines", 8th International Workshop Model-Driven Requirements Engineering (MoDRE), August 2018, affilated with 26th IEEE International Requirements Engineering Conference (RE 2018). (pdf)[IEEEXPLORE]
  2. Simon Hudon, Thai Son Hoang and Jonathan S. Ostroff, “The Unit-B Method — Refinement Guided by Progress Concerns”, Software and Systems Modeling (SoSym), Springer, Volume 15: Issue 4, pp. 1091-1116, October 2016. doi:10.1007/s10270-015-0456-2
  3. Chen-Wei Wang, Jonathan Ostroff and Simon Hudon, "Using Indexed and Synchronous Events to Model and Validate Cyber-Physical Systems", 4th International Workshop on Engineering Safety and Security Systems, ESSS 2015 (affiliated with FM2015), Oslo, June, 2015.
  4. Chen-Wei Wang, Jonathan Ostroff and Simon Hudon, “Precise Documentation and Validation of Requirements”, Formal Techniques for Safety-Critical Systems (revised selected papers from Second International Workshop FTSCS 2013), Communications in Computer and Information Science, Vol. 419, Springer, 2014.
  5. Jonathan S. Ostroff, Chen-Wei Wang, Yang Liu, Jun Sun and Simon Hudon, “TTM/PAT: Specifying and Verifying Timed Transition Models”, in Formal Techniques for Safety? Critical Systems (revised selected papers from Second International Workshop FTSCS 2013), Communications in Computer and Information Science, Vol. 419, Springer, 2014.
  6. Jacques Carette, Chris George, Zarrin Langari, Mark Lawford, Tom Maibaum, Ned Nedialkov, Vera Pantelic, Spencer Smith, Ali Taleghani, Alan Wassyng and Jonathan Ostroff, "Analysis of Critical Scientific Software", CASCON Workshop 2011: Progress on the Certification of Critical Software-Intensive Systems, November 2011. (pdf)
  7. Faraz Torshizi, Jonathan S. Ostroff, Richard F. Paige and Marsha Chechik, "The SCOOP concurrency model in Java‐like languages", Communicating Process Architectures 2009 (CPA2009 at Formal Methods Week 2009), Technische Universiteit Eindhoven, (November 2009).
  8. Jonathan S. Ostroff, Faraz Ahmadi Torshizi,  Hai Feng Huang, and Bernd Schoeller, "Beyond contracts for concurrency", Formal Aspects of Computing, vol. 21:4 (2009), 28 pages (local copy).
  9. Piotr Nienaltowski1 , Bertrand Meyer, and Jonathan S. Ostroff, "Contracts for Concurrency", Formal Aspects of Computing, vol. 21:4 (2009). 14 pages.
  10. Jonathan S. Ostroff and Faraz Ahmadi Torshizi, "Testable Requirements and Specifications", Invited paper, Tests and Proofs - TAP2007, ETH Zurich, February 2007, LNCS 4454 ("Tests and Proofs").
  11. Richard F. Paige, Phil J. Brooke, and Jonathan S. Ostroff. "Metamodel-Based Model Conformance and Multi-View Consistency Checking", ACM Transactions on Software Engineering and Methodology,Vol. 16, No. 3, Article 11, July 2007, 49 pages.
  12. Jonathan S. Ostroff, Chen-Wei Wang, Eric Kerfoot, and Faraz Ahmadi Torshizi,  "Automated Model-based Verification of Object-Oriented Code", Microsoft Report MSR-TR-2006-117 of Workshop on Verified Software: Theory, Tools, and Experiments 2006 (VSTTE 2006, as part of FLoC 2006), Seattle, August 22, 2006.
  13. Jonathan S. Ostroff, Chen-Wei Wang, Faraz Ahmadi Torshizi, and Eric Kerfoot, "ES-Verify: A Tool for Automated Model-based Verification of Object-Oriented Code", Formal Methods 2006 Posters & Research Tools (FM'06), McMaster University, Canada, August 2006.
  14. Jonathan S. Ostroff, Faraz Torshizi and Hai Feng Huang, "Verifying Properties Beyond Contracts of SCOOP Programs", York Report YCS 405, First International Symposium on Concurrency, Real-Time and Distribution in Eiffel-like Languages (CORDIE'06), York UK, July 2006.
  15. Faraz Ahmadi Torshizi and Jonathan S. Ostroff: ESpec -- a Tool for Agile Development via Early Testable Specifications, Technical Report CS-2006-04, York University.
  16. Jonathan S. Ostroff, Richard F. Paige, David Makalsky and Phillip J. Brooke. E-Tester: a Contract-Aware and Agent-Based Unit Testing Framework for Eiffel. Journal of Object Technology, Volume 4 Number 7, Sep-Oct 2005.
  17. Ali Taleghani and Jonathan S. Ostroff. Contractual consistency of BON static and dynamic diagrams. To appear in  International Workshop on Software Verification and Validation (SVV 2004 in conjunction with ICFEM'04), Seattle (USA), November 8 2004.
  18. Richard Paige, Phillip J. Brooke, Jonathan S. Ostroff. Specification Driven Development of an Executable Metamodel in Eiffel. Proc. 2004 Workshop WS5 on Software Model Engineering (WiSME'04) at the 7th International Conference on the UML October 11-15 2004, Lisbon, Portugal. (slides) (This is a longer version of the extended abstract in ISSRE'04 below.)
  19. Richard F. Paige, Jonathan S. Ostroff and  Phillip J. Brooke. Agile Development of a Metamodel in Eiffel. To appear in Supplementary Proceedings of the 15th IEEE International Symposium on Software Reliability Engineering (ISSRE 2004), 2-5 November 2004, Saint-Malo, Bretagne, France.
  20. Richard F. Paige and Jonathan .S. Ostroff. Specification-Driven Design for Teaching Lightweight Formal Methods, Proc. Teaching Formal Methods: CoLogNET/FME Symposium, TFM 2004, Ghent, Belgium, November 18-19, 2004, LNCS 3294, pages 107-123, Springer-Verlag,  2004 (pdf).
  21. Jonathan S. Ostroff, David Makalsky and Richard Paige. Agile Specification Driven Development. Fifth International Conference on Extreme Programming and Agile Processes in Software Engineering XP2004, June 6-10, 2004, Garmisch-Partenkirchen, Germany.
  22. Nati Fuks, Jonathan S. Ostroff and Richard Paige.  SCOOP to Eiffel Code Generator. Journal of Object Technology, Vol 3 No. 10 Nov/Dec, 2004.
  23. R.F. Paige and J.S. Ostroff. ERC: an Object-Oriented Refinement Calculus for Eiffel, Formal Aspects of Computing, Vol 16, pages 51-79, Springer-Verlag, April 2004.
  24. Ali Taleghani and Jonathan S. Ostroff. The BON Development Tool. Proc. Eclipse Technology eXchange eTX/OOPSLA'03, Anaheim, CA, October 2003.
  25. R.F. Paige, J.S. Ostroff, and P.J. Brooke. A Test-Based Agile Approach to Checking the Consistency of Class and Collaboration Diagrams. UK Software Testing Workshop II, University of York, 4-5 September 2003.
  26. R.F. Paige, J.S. Ostroff, and P.J. Brooke. Formalising Eiffel Reference and Expanded Types in PVS,  Proc. International Workshop on Aliasing, Confinement, and Ownership in Object-Oriented Programming (IWACO), co-located with ECOOP 2003, Darmstadt, Germany, July 2003.
  27. Richard F. Paige, Jonathan S. Ostroff and  Phillip J. Brooke. Theorem Proving Support for View Consistency Checking. L'OBJET: Software, Databases, Networks 9(4): pages 115-134, 2003. [This is a journal version of the ROOM4 conference paper below].
  28. Richard Paige and Jonathan S. Ostroff. The Single Model Principle. Journal of Object Oriented Technology. Vol 1 No. 5, 2002  (invited contribution).
  29. R.F. Paige, L. Kaminskaya, J.S. Ostroff, and J. Lancaric. BON-CASE: an Extensible CASE Tool for Formal Specification and Reasoning, to appear in Proc. TOOLS USA 2002, Santa Barbara, CA, USA, July 2002. (republished in Journal of Object Technology - JOT - Vol. 1, No. 3, p77-96, August 2002 pdf).
  30. R.F. Paige, J.S. Ostroff, and P.J. Brooke. Checking the Consistency of Class and Collaboration Diagrams using PVS, in Proc. Fourth Workshop on Rigorous Object-Oriented Methods (ROOM4), London, England, British Computer Society, March 2002. (pdf). (slides)
  31. R.F. Paige and J.S. Ostroff. A Seamless Eiffel-Based Refinement Calculus for Object-Oriented Systems, in Proc. Workshop on Refinement of Critical Systems 2002 (co-located with ZB-2002), Grenoble, France, January 2002.
  32. R.F. Paige and J.S. Ostroff. The Single Model Principle, in Proc. Requirements Engineering '01 (RE'01), Toronto, Canada, IEEE Press, August 2001.
  33. R.F. Paige and J.S. Ostroff. A Proposal for a Lightweight Rigorous UML-Based Development Method for Reliable Systems, in Proc. Workshop on Practical UML-Based Rigorous Development Methods 2001 (co-located with UML 2001), p192-207, Toronto, Canada, Lecture Notes in Informatics (GI Series), German Society, October 2001.
  34. R.F. Paige and J.S. Ostroff. Metamodelling and Conformance Checking with PVS, in Proc. Fundamental Aspects of Software Engineering (FASE'01), Genoa, Italy, LNCS 2029, p2-16, Springer-Verlag, April 2001. (This is a shortened version of the above technical report.)
  35. J.S. Ostroff and R.F. Paige. The Logic of Software Design. IEE Proceedings - Software Engineering 147(3):73-80, October 2000 (PDF).
  36. R.F. Paige, J.S. Ostroff, and P.J. Brooke. Principles of Modeling Language design, Information and Software Technology. No 42, pages 665-675, 2000.
  37. Richard Paige and Jonathan S. Ostroff . Producing Reliable Software via the Single Model Principle. Technical Report CS-2001-02, Department of Computer Science, York University.
  38. Ostroff, J.S. Composition and Refinement of Discrete Real-Time Systems. ACM Trans. on Software Engineering Methodology, 8(1): 1-48, 1999.
  39. Paige, R.F. and J.S. Ostroff. A Comparison of Business Object Notation and the Unified Modeling Language. In Proc. Second International Conference on the Unified Modeling Language (UML'99), Springer-Verlag, LNCS 1723, 67--82, 1999. (extended version)
  40. Paige, R.F. and J.S. Ostroff. Developing BON as an Industrial-Strength Formal Method. In Proc. World Congress on Formal Methods (FM'99), Springer-Verlag, LNCS 1708, 1999.
  41. Ostroff, J.S. and R.F. Paige. Formal Methods in the Classroom. In Proc. 3rd IEEE Real-Time Systems Education Workshop, Poznam, Poland, IEEE Press, 63--70, 1998. (extended version)
  42. Paige, R. and J.S. Ostroff. From Z to Bon/Eiffel. In 13th IEEE international Conference on Automated Software Engineering (ASE), Hawaii, IEEE Computer Society, 1998. www.cs.yorku.ca/techreports/1998/CS-98-05.html
  43. Ostroff, J.S. and R. Paige. The Logic of Software Design. Computer Science, York University. CS-98-04, 1998. http://www.cs.yorku.ca/General/techreports/1998/CS-98-04.html
  44. Ostroff, J.S. A Visual Toolset for the Design of Real-Time Discrete Event Systems. IEEE Trans. on Control Systems Technology, 5(3): 320-337, 1997. IEEE-1997-Visual.pdf
  45. Lawford, M., J.S. Ostroff, and W.M. Wonham. Model Reduction of Modules for State-Event Temporal Logics. In IFIP Joint International Conference on Formal Description Techniques (FORTE-PSTV'96), Chapman & Hall, 1996.
  46. Ostroff, J.S. and H.K. Ng. The Design of Real-Time Systems Using Standard Untimed Theories. In Preprints Third AMAST Workshop on Real-Time Systems, Salt Lake City, Utah, ONR and Iowa University, 1996.
  47. Ostroff, J.S. A CASE Tool for the Design of Safety-Critical Systems. In Proc. Seventh International Workshop on Computer Aided Software Engineering CASE'95, IEEE Computer Society Press, 370-380 (see also http://www.cs.yorku.ca/pub/ostroff/papers.95/case95.extended.pdf for an extended version of the paper), 1995.
  48. Ostroff, J.S. Automated Modular Specification and Verification of Real-Time Reactive Systems. In Proc. Workshop on Industrial Strength Formal Specification Techniques WIFT'95, IEEE Computer Society Press, 108-121, 1995.
  49. Ostroff, J.S. Visual Tools for Verifying Real-Time Systems. In Theories and Experiences for Real-Time System Development, 83-101. AMAST Series in Computing: Vol. 2. World Scientific Publishing Company, 1994.
  50. Ostroff, J.S. Specifying and Verifying Real-Time Reactive Systems in TTM/RTTL. Dep. of Computer Science, York University. CS-ETR-94-08, 1994.
  51. Ostroff, J.S. Automated Modular Specification and Verification of Real-Time Reactive Systems. Dept. of Computer Science, York University, Canada. CS-ETR-94-06, 1994.
  52. Lawford, M., W.M. Wonham, and J.S. Ostroff. State-Event Labels for Labelled Transition Systems. In Proc. 33rd IEEE Conference on Decision and Control, Orlando, FL, IEEE Control System Society, 3642-3648, 1994.
  53. Ostroff, J.S. A Verifier for Real-Time Properties. Real-Time Journal, 4:5–35, 1992.
  54. Ostroff, J.S. Verification of Safety Critical Systems Using TTM/RTTL. In REX Real-Time: Theory in Practice, LNCS 600 Springer-Verlag, 1992.
  55. Ostroff, J.S. Design of Real-Time Safety Critical Systems. The Journal of Systems and Software, 18(1): 33–60, 1992.
    Republished in: High-Integrity System Specification and Design, editors Jonathan P. Bowen and Michael G. Hinchey, Springer-Verlag London Ltd, 1999.
  56. [20] Ostroff, J.S. StateTime — a Diagrammatic Toolset for the Design and Verification of Real-Time Systems. Department of Computer Science, York University. TR CS-92-07, 1992.
  57. [21] Ostroff, J.S. Systematic Development of Real-Time Discrete Event Systems. In Proceedings of the ECC91 European Control Conference, Grenoble, Hermes Press, 522–533, 1991.
  58. [22] Ostroff, J.S. Constraint Logic Programming for Reasoning about Discrete Event Processes. The Journal of Logic Programming, 11(3 and 4): 243 --270, 1991.
  59. [23] Ostroff, J.S. Deciding properties of Timed Transition Models. IEEE Transactions on Parallel and Distributed Systems, 1(2): 170-183, 1990.
  60. [24] Ostroff, J.S. A Logic for Real-Time Discrete Event Processes. IEEE Control Systems Magzine, 1990.
  61. [25] Ostroff, J.S. and W.M. Wonham. A Framework for Real-Time Discrete Event Control. IEEE Transactions on Automatic Control, 35(4): 386–397, 1990.
  62. [26] Ostroff, J.S. Automatic verification of timed transition systems. In Proceedings of the Workshop on Automatic Verification Methods for Finite State Systems, Springer-Verlag, Lecture Notes in Computer Science, 1989.
  63. [27] Ostroff, J.S. Temporal Logic for Real-Time Systems. Advanced Software Development Series, ed. J. Kramer. Research Studies Press Limited (distributed by John Wiley and Sons), England, 1989.
  64. [28] Ostroff, J.S. Synthesis of controllers for real-time discrete event systems. In Proceedings of the 28th IEEE Conference on Decision and Control, 1989.
  65. [29] Ostroff, J.S. Mechanizing the verification of real-time discrete systems. In Proceedings of the 15th Symposium on Microprocessing and Microprogramming, North-Holland, 1989.
    [30] Ostroff, J.S. Real-time temporal logic decision procedures. In Proceedings of 10th IEEE Real-Time Systems Symposium, Santa Monica, Ca: 1989.
  66. [31] Ostroff, J.S. Verification of finite state real-time distributed processes. In Proceedings of 9th IEEE International Conference on Distributed Computing Systems, 207-216. 1989.
    [32] Ostroff, J.S. Modularity in the ESM/RTL framework. In Software for Computer Control 1988 (Selected papers from 5th IFAC/IFIP Symposium SOCOCO'88), 15-20. Oxford: Pergamon Press, 1989.
  67. [33] Ostroff, J.S. Modular Reasoning in the ESM/RTL framework for Real-time Software. Department of Computer Science, York University, Canada. CS-88-03, 1988.
  68. [34] Ostroff, J.S. Temporal Logic and extended state machines in discrete event control. In Advanced computing concepts and techniques in control engineering, 215-236. 47. Springer-Verlag, 1988.
  69. [35] Ostroff, J.S. and W.M. Wonham. Modelling, Specifying and Verifying Real-time Embedded Computer Systems. In Proceedings of the 8th IEEE Real-Time Systems Symposium, 124-132. San Jose: 1987.
  70. [36] Ostroff, J.S. and W.M. Wonham. State Machines, Temporal Logic and Control: a Framework for Discrete Event Systems. In Proceedings of the 26th IEEE Conference on Decision and Control, 681-686. Los Angeles: 1987.
  71. [37] Ostroff, J.S. Real-time Computer Control of Discrete Event Systems Modelled by Extended State Machines: a Temporal Logic Approach. Systems Control Group, University of Toronto. 8618, 1986.
  72. [38] Ostroff, J.S. and W.M. Wonham. A temporal logic approach to real time control. In 24th IEEE Conference on Decision and Control, Florida, 656-657, 1985.

 

 

Bertrand Meyer's gallery of computer scientists

ACM publications

SEL home page

Faraz Torshizi home page

http://jonathan.ostroff.name

Linked In URL

Namyz