Shinya Umeno

home | publications | cv | dblp

[Journal Paper]

Myla Archer, HongPing Lim, Nancy Lynch, Sayan Mitra and Shinya Umeno. Specifying and proving properties of timed I/O automata using Tempo. Design Automation for Embedded Systems, 12(1-2):139-170, 2008. [LINK]

[Refereed Conference Papers]

Shinya Umeno and Nancy Lynch. Automated Formal Verification of the DHCP Failover Protocol Using Timeout Order Abstraction. To appear in Proceedings of 15th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2010), Oxford, UK, March 22-26 2010. [PDF] [FILES]
Shinya Umeno. Machine-Assisted Parameter Synthesis of the Biphase Mark Protocol Using Event Order Abstratcion. In The 7th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 2009), Budapest, Hungry, September 13-16, 2009. [PDF] [FILES]
Shinya Umeno. Event Order Abstraction for Parametric Real-Time System Verification. The 8th ACM & IEEE International Conference on Embedded Software (EMSOFT 2008), Atlanta, Georgia, October 19 - 24, 2008, pages 1-10. [PDF (refined version)] [BIB]
Shinya Umeno and Nancy Lynch. Safety Verification of an Aircraft Landing Protocol: A Refinement Approach. Hybrid Systems: Computation and Control (HSCC 2007), Pisa, Italy, April 3-5, 2007, volume 4416 of Lecture Notes in Computer Science, pages 557-572. [PDF] [BIB]
Shinya Umeno and Nancy Lynch. Proving Safety Properties of an Aircraft Landing Protocol Using I/O Automata and the PVS Theorem Prover: A Case Study. FM 2006: Formal Methods, International Symposium of Formal Methods Europe, Hamilton, Ontario Canada, August, 2006. Volume 4085 of Lecture Notes in Computer Science, pages 64-80, Springer, 2006. [PDF] [BIB]
Myla Archer, HongPing Lim, Nancy Lynch, Sayan Mitra and Shinya Umeno. Specifying and Proving Properties of Timed I/O Automata in the TIOA Toolkit. Fourth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'06), Napa Valley, California, July, 2006. [PDF] [BIB]

[Technical Report]

Shinya Umeno. Event Order Abstraction for Parametric Real-Time System Verification. MIT-CSAIL-TR-2008-048, Massachusetts Institute of Technology, July, 2008. (This is a technical report version of the EMSOFT 2008 paper.) [LINK]

[Master's Thesis]

Shinya Umeno. Proving Safety Properties of an Aircraft Landing Protocol Using Timed and Untimed I/O Automata: A Case Study. Masters Thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA, October, 2006. [PDF] [BIB]