Modeling and Specification.-
Orchestration Combinators in Apla+ Language.- On Termination and Boundedness of Nested Updatable Timed Automata.- Instant-based and State-based Analysis of Infinite Logical Clock.-
Animation and Prototyping.-
Automated Safety Analysis on Scenario-based Requirements for Train Control System.- A Case Study of a GUI-Aided Approach to Constructing Formal Specifications.- Formal Development of Linear Structure Reusable Components in PAR Platform.-
Verification and Validation.-
E-SSL:An SSL Security-Enhanced Method for Bypassing MITM Attacks in Mobile Internet.- A Proof System for MSVL Programs in Coq.- Runtime Verification Monitor Construction for Three-valued PPTL.- Applying SOFL to a Railway Interlocking System in Industry.
