3. TASE 2009: Tianjin, China

Invited Talks

• Kim Guldstrand Larsen:
  Verification and Performance Analysis for Embedded Systems. 3-4
  
• Zhong Shao:
  Modular Development of Certified System Software. 5
  

Invited Tutorial

• Jin Song Dong, Jun Sun:
  Towards Expressive Specification and Efficient Model Checking. 9
  

Real-Time and Embedded Systems

• Hugh Anderson, Siau-Cheng Khoo:
  Improving Responsiveness of Hard Real-Time Embedded Systems. 13-20
  
• Guoqiang Li, Shoji Yuen, Masakazu Adachi:
  Environmental Simulation of Real-Time Systems with Nested Interrupts. 21-28
  
• Istvan Knoll, Anders P. Ravn, Arne Skou:
  Semantics for Communicating Actors with Interdependent Real-Time Deadlines. 29-35
  
• Yan Xiao, Zhenhua Duan, Pengcheng Nie:
  An Efficient Algorithm for Finding Empty Space for Reconfigurable Systems. 36-43
  

Semantics

• Andrew Butterfield, Pawel Gancarski, Jim Woodcock:
  State Visibility and Communication in Unifying Theories of Programming. 47-54
  
• Lijun Shan, Hong Zhu:
  Semantics of Metamodels in UML. 55-62
  
• T. M. Rabehaja, J. W. Sanders:
  Refinement Algebra with Explicit Probabilism. 63-70
  

Model Checking

• Hong Pan, Yi Lv, Huimin Lin:
  Environment Abstraction with State Clustering and Parameter Truncating. 73-80
  
• Yang Liu, Jun Pang, Jun Sun, Jianhua Zhao:
  Verification of Population Ring Protocols in PAT. 81-89
  
• Wei Chen, Wenhui Zhang:
  Bounded Model Checking of ACTL Formulae. 90-99
  

Specification and Security

• Richard Banach:
  Coarse Grained Retrenchment and the Mondex Denial of Service Attacks. 103-110
  
• Xiangpeng Zhao, Jianwen Su, Hongli Yang, Zongyan Qiu:
  Enforcing Constraints on Life Cycles of Business Artifacts. 111-118
  
• Hai-Feng Guo, Wen Zheng, Mahadevan Subramaniam:
  Consistency Checking for LSC Specifications. 119-126
  
• Jun Sun, Yang Liu, Jin Song Dong, Chunqing Chen:
  Integrating Specification and Programs for System Modeling and Verification. 127-135
  

Software Testing I

• Gwan-Hwan Hwang, Che-Sheng Lin, Li-Te Tsao, Kuei-Huan Chen, Yan-You Li:
  A Framework and Language Support for Automatic Dynamic Testing of Workflow Management Systems. 139-146
  
• Bernhard K. Aichernig, Farhad Arbab, Lacramioara Astefanoaei, Frank S. de Boer, Sun Meng, Jan J. M. M. Rutten:
  Fault-Based Test Case Generation for Component Connectors. 147-154
  
• Zheng Wang, Xiao Yu, Tao Sun, Geguang Pu, Zuohua Ding, Jueliang Hu:
  Test Data Generation for Derived Types in C Program. 155-162
  

Software Models

• Bernd Fischer, Ando Saabas, Tarmo Uustalu:
  Program Repair as Sound Optimization of Broken Programs. 165-173
  
• Bo Song, Huaikou Miao:
  Modeling Web Applications and Generating Tests: A Combination and Interactions-guided Approach. 174-181
  
• Stephen Barrett, Daniel Sinnig, Patrice Chalin, Greg Butler:
  Merging of Use Case Models: Semantic Foundations. 182-189
  

Verification

• Yuan-Fang Li, Jing Sun, Gillian Dobbie, Scott Uk-Jin Lee, Hai H. Wang:
  Verifying Semistructured Data Normalization Using SWRL. 193-200
  
• Yuxin Deng, Jean-François Monin:
  Verifying Self-stabilizing Population Protocols with Coq. 201-208
  
• Xinyu Jiang, Yu Guo, Yiyun Chen:
  The Logical Approach to Low-Level Stack Reasoning. 209-216
  
• Shikun Chen, Zhoujun Li, Mengjun Li:
  Constructing Program Invariants via Solving QBF. 217-221
  

Concurrency

• Moritz Martens, Mila E. Majster-Cederbaum:
  Using Architectural Constraints for Deadlock-Freedom of Component Systems with Multiway Cooperation. 225-232
  
• Ming Fu, Yu Zhang, Yong Li:
  Formal Reasoning about Concurrent Assembly Code with Reentrant Locks. 233-240
  
• Weisong Li:
  Algorithms for Computing Weak Bisimulation Equivalence. 241-248
  

Software Testing II

• Mariëlle Stoelinga, Mark Timmer:
  Interpreting a Successful Testing Process: Risk and Actual Coverage. 251-258
  
• Tim A. Majchrzak, Herbert Kuchen:
  Automated Test Case Generation Based on Coverage Analysis. 259-266
  
• Lian Yu, Wei Zhao, Xiangdong Fan, Jun Zhu:
  Exploring Topological Structure of Boolean Expressions for Test Data Selection. 267-274
  
• Guy-Vincent Jourdan, Gregor von Bochmann:
  On Testing 1-Safe Petri Nets. 275-281
  

Poster Papers

• Moritz Kleine, Björn Bartels, Thomas Göthel, Sabine Glesner:
  Verifying the Implementation of an Operating System Scheduler. 285-286
  
• Shengyi Wang, Zongyan Qiu:
  A Tool for Estimating Memory Usage. 287-288
  
• Tannaz Alinaghi, Camellia Ghoroghi, Ahmad Saborui, Reza Basseda:
  A Framework for Dependency Evaluation of the Agent Oriented Methodologies Work Flows. 289-290
  
• Che-Sheng Lin, Gwan-Hwan Hwang:
  Spontaneous Detection of Infinite Loops and Livelocks in Dynamic Testing of Concurrent Programs. 291-292
  
• Hehua Zhang, Stephan Merz, Ming Gu:
  Specifying and Verifying PLC Systems with TLA+. 293-294
  
• Pierre Kelsen, Qin Ma:
  Domain Hierarchies: A Basic Theoretical Framework for Integrating Software Domains. 295-296
  
• Minghui Wu, Fanwei Zhu, Jia Lv, Tao Jiang, Jing Ying:
  Improve Semantic Web Services Discovery through Similarity Search in Metric Space. 297-298
  
• Yanfang Ma, Min Zhang, Yixiang Chen:
  Parameterized Bisimulation Infinite Evolution Mechanism. 299-300
  
• Wen Su, Fan Yang, Huibiao Zhu, Qin Li:
  Modeling MapReduce with CSP. 301-302
  
• Tetsuya Mizutani, Tatsuo Suzuki, Masayuki Shio, Yasuwo Ikeda:
  Formal Specification and Experiments of an Expressive Human-Computer Ensemble System with Rehearsal. 303-304
  
• S. Asadollahi, Vahid Rafe, Reza Rafeh, Adel Torkaman Rahmani:
  Towards Automated Software Verification Using Model Checking Techniques. 305-306
  
• Rhys Owen, Hugh Anderson:
  Data Structure Shape Inference and Verification for OO Programs. 307-308
  
• Jinwei Wang, Huazhi Sun, Jianping Fan:
  DUMS: A Dynamical Updatable Monitoring System for Desktop PCs Used for Distributed Computing. 309-310
  
• Tetsuya Mizutani, Shigeru Igarashi, Yasuwo Ikeda, Masayuki Shio:
  Formal Representation and Analysis of a Near Miss Accident in N Sigma-labeled Calculus. 311-312
  
• Saqib Iqbal, Gary Allen:
  Representing Aspects in Design. 313-314
  
• Dong-Wook Kim, Tae-Sung Jung, Dae-Won Kim, Seong-Hyeuk Nam, Hyuk-Ryul Kwon, Sang-Haeng Choi, Hyung-Dae Koh, Han-Suk Choi, Hong-Seog Park:
  G-BLAST: BLAST Manager in an Heterogeneous Distributed Environment. 315-316
  
• Dehui Du, Ling Yin:
  Probabilistic Coordination Language for Component Dynamic Composition. 317-318
  
• Farzaneh Mahdian, Vahid Rafe, Reza Rafeh, Adel Torkaman Rahmani:
  Modeling Fault Tolerant Services in Service-Oriented Architecture. 319-320
  
• Guanhua He, Chenguang Luo:
  Heap Memory Requirements Analysis via Separation Logic. 321-322
  
• Cristian Gherghina, Cristina David:
  Automated Verification Using Unified Control Flows. 323-324
  
• Qichao Liu, Faizan Javed, Marjan Mernik, Barrett R. Bryant, Jeff Gray, Alan P. Sprague, Dejan Hrncic:
  MARS: Metamodel Recovery from Multi-tiered Models Using Grammar Inference. 325-326
  
• Jieqi Ding, Han Zhu, Huibiao Zhu, Qin Li:
  Formal Approaches to Deadlock Analysis in Competitions of Shared Web Resources. 327-328
  
• Jueliang Hu, Zuohua Ding, Jing Liu, Ling Yin:
  Measuring the Survivability of Object-Oriented Software. 329-330