Testing with Buchi Automata: Transition Coverage Metrics, Performance Analysis, and Property Refinement -- Forward and Backward Analysis of Weak Sequencing Specification -- A CEGAR Tool for the Reachability Analysis of PLC-Controlled Plants using Hybrid Automata -- On the Formalization of Cardinal Points of Optical Systems -- Towards a General Model to Handle Multi-Enabledness in Time Petri Nets -- Time Properties Verification of Real-Time Systems using UML/MARTE/OCL-RT -- Formal Modeling and Analysis of Business Process Timed Constraints -- A Model-based Approach for User Requirements Decomposition and Component Selection.