Abstract is missing.
- Towards Structuring System Specifications with Time Bands Using Layers of Rely-Guarantee ConditionsIan J. Hayes. 1-2 [doi]
- With an Open Mind: How to Write Good ModelsCyrille Artho, Koji Hayamizu, Rudolf Ramler, Yoriyuki Yamagata. 3-18 [doi]
- Model-Based Testing from Controlled Natural Language RequirementsGustavo Carvalho, Flávia de Almeida Barros, Florian Lapschies, Uwe Schulze, Jan Peleska. 19-35 [doi]
- An UPPAAL Framework for Model Checking Automotive Systems with FlexRay ProtocolXiaoyun Guo, Hsin-hung Lin, Kenro Yatake, Toshiaki Aoki. 36-53 [doi]
- Early Analysis of Soft Error Effects for Aerospace Applications Using Probabilistic Model CheckingKhaza Anuarul Hoque, Otmane Aït Mohamed, Yvon Savaria, Claude Thibeault. 54-70 [doi]
- A Strand Space Approach to Provable AnonymityYongjian Li, Jun Pang. 71-87 [doi]
- Counterexample Generation for Hybrid AutomataJohanna Nellen, Erika Ábrahám, Xin Chen 0002, Pieter Collins. 88-106 [doi]
- TTM/PAT: Specifying and Verifying Timed Transition ModelsJonathan S. Ostroff, Chen-Wei Wang, Simon Hudon, Yang Liu, Jun Sun 0001. 107-124 [doi]
- Formalizing and Verifying Function Blocks Using Tabular Expressions and PVSLinna Pang, Chen-Wei Wang, Mark Lawford, Alan Wassyng. 125-141 [doi]
- Reflections on Verifying Software with WhileyDavid J. Pearce, Lindsay Groves. 142-159 [doi]
- Compositional Nonblocking Verification with Always Enabled Events and Selfloop-Only EventsColin Pilbrow, Robi Malik. 160-177 [doi]
- Formal Semantics and Analysis of Timed Rebeca in Real-Time MaudeZeynab Sabahi-Kaviani, Ramtin Khosravi, Marjan Sirjani, Peter Csaba Ölveczky, Ehsan Khamespanah. 178-194 [doi]
- On the Cloud-Enabled Refinement Checking of Railway Signalling InterlockingsAndrew Simpson, Jaco Jacobs. 195-211 [doi]
- Parametric Schedulability Analysis of Fixed Priority Real-Time Distributed SystemsYoucheng Sun, Romain Soulat, Giuseppe Lipari, Étienne André, Laurent Fribourg. 212-228 [doi]
- Wind Turbine System: An Industrial Case Study in Formal Modeling and VerificationJagadish Suryadevara, Gaetana Sapienza, Cristina Cerschi Seceleanu, Tiberiu Seceleanu, Stein Erik Ellevseth, Paul Pettersson. 229-245 [doi]
- Refinement Tree and Its Patterns: A Graphical Approach for Event-B ModelingKriangkrai Traichaiyaporn, Toshiaki Aoki. 246-261 [doi]
- Precise Documentation and Validation of RequirementsChen-Wei Wang, Jonathan S. Ostroff, Simon Hudon. 262-279 [doi]
- Certainly Unsupervisable StatesSimon Ware, Robi Malik, Sahar Mohajerani, Martin Fabian. 280-296 [doi]