Model-based development - OMG Model Driven Architecture (DMA) Middleware www.omg.org/mda/mda_files/cds01021.pdf - CORBA ORB - Java RMI - middleware standards based on XML and SOAP (Simple Object Access Protocol) Real-time and Embedded Systems - H. Kopetz, Software engieering for real-time systems: a roadmap, Proceedings of the Conference on the Future of Software Engineering, Limerick, Ireland 2000, pp. 201-211. (http://dream.eng.uci.edu/ece198/serious.htm) - Time Trigger Architecture - Kim, K.H., "Object Structures for Real-Time Systems and Simulators", IEEE Computer, August 1997, pp.62-70. (http://dream.eng.uci.edu/TMO/TMO.htm) Witness Generation: 1. Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking (1994) E. Clarke, O. Grumberg, K. McMillan, X. Zhao 32nd Design Automation Conference (DAC 95) 2. Vacuity Detection in Temporal Model Checking (1999) Orna Kupferman, Moshe Y. Vardi Conference on Correct Hardware Design and Verification Methods 3. Efficient Detection of Vacuity in Temporal Model Checking Ilan Beer and Shoham Ben-David and Cindy Eisner and Yoav Rodeh Formal Methods in System Design, volume = "18", Pages 141-163, 2001 Specification Patterns: - www.cis.ksu.edu/santos/spec-patterns/ - Property Specification Patterns for Finite-state Verification, Matthew B. Dwyer, George S. Avrunin and James C. Corbett, in the 2nd Workshop on Formal Methods in Software Practice, March, 1998. - Patterns in Property Specifications for Finite-state Verification, Matthew B. Dwyer, George S. Avrunin and James C. Corbett, Proceedings of the 21st International Conference on Software Engineering, May, 1999. Other Topics: - Bounded Model Checking: - Specification/model-based test generation - Formal modeling of schedulability: - UML-RT, etc.: (http://www4.in.tum.de/~csduml02/) - Embedded system co-design paradigms: - Real-Time Java: