|
Day 1: 29 July 2009
8:00- 8:45: Registration
8:45- 8:55: Welcome session
8:55- 9:10: Photo session
9:10-10:10: Invited Talk (Chair: Huibiao Zhu)
Verification and Performance Analysis of Embedded Systems
Kim G. Larsen ( Aalborg University )
10:10-10:35: (Chair: Huibiao Zhu)
Improving Responsiveness of Hard Real-Time Embedded Systems
Hugh Anderson (Wellington Institute of Technology) and Siau-Cheng KHOO ( National University of Singapore )
10:35-11:05 Coffee Break
11:05-12:20: Session 1 : Real-Time and Embedded Systems (Jun Sun)
Environmental Simulation of Real-Time Systems with Nested Interrupts
Guoqiang Li ( Shanghai Jiao Tong University ), Shoji Yuen ( Nagoya University ) and Masakazu Adachi ( Toyota Central R&D Labs. INC.).
Semantics for Communicating Actors with Interdependent Real-Time Deadlines
István Knoll ( Aalborg University ), Anders P. Ravn ( Aalborg University ) and Arne Skou ( Aalborg University ).
An Efficient Algorithm for Finding Empty Space for Reconfigurable Systems
Zhenhua Duan ( Xidian University ) and Yan Xiao ( Xidian University ).
12:20-14:00: Lunch
14:00-15:15: Session 2 : Semantics (Chair: Zongyan Qiu)
State Visibility and Communication in Unifying Theories of Programming
Andrew Butterfield ( Trinity College Dublin ), Pawel Gancarski ( Trinity College Dublin ) and Jim Woodcock ( University of York ).
Semantics of Metamodels in UML
Lijun Shan ( National University of Defence Technology) and Hong Zhu ( Oxford Brookes University ).
Refinement algebra with explicit probabilism
Tahiry Rabehaja (UNU/IIST) and Jeffrey Sanders (UNU/IIST).
15:15-16:15: Poster Session I (Chair: Hugh Anderson)
(Poster Papers in Annex A )
16:15-17:30: Session 3 : Model Checking (Chair: Kim Larsen)
Environment Abstraction with State Clustering and Parameter Truncating
Hong Pan (Institute of Software, Chinese Academy of Sciences), Yi Lv (Institute of Software, Chinese Academy of Sciences) and Huimin Lin (Institute of Software, Chinese Academy of Sciences).
Verification of Population Ring Protocols in PAT
Yang Liu ( National University of Singapore ), Jun Pang ( University of Luxembourg ), Jun Sun ( National University of Singapore ) and Jianhua Zhao ( Nanjing University ).
Bounded Model Checking of ACTL formulae
Wei Chen ( Institute of Software , Chinese Academy of Sciences) and Wenhui Zhang ( Institute of Software , Chinese Academy of Sciences).
18:30: Reception
Day 2: 30 July 2009
9:00-10:00: Invited Talk (Chair: Shengchao Qin)
Modular Development of Certified System Software
Zhong Shao ( Yale University )
10:00-10:25: (Chair: Shengchao Qin)
Coarse Grained Retrenchment and the Mondex Denial of Service Attacks
Richard Banach ( Manchester University ).
10:25-11:00: Coffee Break
11:00-12.15: Session 4: Specification (Chair: Zhong Shao)
Specifying and Enforcing Constraints of Artifact Life Cycles
Xiangpeng Zhao (Peking University), Jianwen Su (University of California at Santa Barbara), Hongli Yang (Beijing University of Technology) and Zongyan Qiu (Peking University).
Consistency Checking for LSC Specifications
Hai-Feng Guo ( University of Nebraska at Omaha ), Wen Zheng ( University of Nebraska at Omaha ) and Mahadevan Subramaniam ( University of Nebraska at Omaha ).
Integrating Specification and Programs for System Modeling and Verification
Jun Sun (National University of Singapore), yang liu (National University of Singapore), jin song dong (National University of Singapore) and Chunqing Chen (National University of Singapore).
12:15-14:00 Lunch
14:00-15:15: Session 5 : Software Testing I (Chair: Richard Banach)
A Framework and Language Support for Automatic Dynamic Testing of Workflow Management Systems
Gwan-Hwan Hwang ( National Taiwan Normal University ), Che-Sheng Lin ( National Taiwan Normal University ), Li-Te Tsao ( National Taiwan Normal University ), Kuei-Huan Chen ( National Taiwan Normal University ) and Yan-You Li ( National Taiwan Normal University ).
Fault-based Test Case Generation for Component Connectors
Bernhard Aichernig (Graz University of Technology), Farhad Arbab (CWI), Lacramioara Astefanoaei (CWI), Frank de Boer (CWI), Meng Sun (CWI) and Jan Rutten (CWI).
Test Data Generation for Derived Types in C Program
Zheng Wang ( East China Normal University ), Xiao Yu ( East China Normal University ), Tao Sun ( East China Normal University ), Geguang Pu ( East China Normal University ) and Zuohua Ding ( Zhejiang Sci-Tech University ).
15:15-16:15: Poster Session II (Chair: Hugh Anderson)
(Poster Papers in Annex B )
16:15-17:30: Session 6 : Software Models (Chair: Haifeng Guo)
Program Repair as Sound Optimization of Broken Programs
Bernd Fischer ( University of Southampton ), Ando Saabas ( Tallinn University of Technology) and Tarmo Uustalu ( Tallinn University of Technology).
Modeling Web Applications and Generating Tests: A Combination and Interactions-guided Approach
Bo Song ( Shanghai University ) and Huaikou Miao ( Shanghai University ).
Merging of Use Case Models: Semantic Foundations
Stephen Barrett ( Concordia University ), Daniel Sinnig ( Concordia University ), Patrice Chalin ( Concordia University ) and Greg Butler ( Concordia University ).
18:30 Banquet
Day 3: 31 July 2009
9:00-10:00: Invited Tutorial (Chair: Shengchao Qin)
Towards Expressive Specification and Efficient Model Checking
Jin Song Dong ( National University of Singapore )
10:00-10:30: Coffee Break
10:30-12:10: Session 7 : Verification (Chair: Jin Song Dong)
Verifying Semistructured Data Normalization using SWRL
Yuan Fang Li (University of Queensland), Jing Sun (University of Auckland), Gillian Dobbie (University of Auckland), Scott Uk-Jin Lee (University of Auckland) and Hai H. Wang (Aston University).
Verifying self-stabilizing population protocols with Coq
Yuxin Deng ( Shanghai Jiao Tong University ) and Jean-francois Monin (Université de Grenoble).
The Logical Approach to Low-level Stack Reasoning
Xinyu Jiang ( University of Science and Technology of China ), Yu Guo ( University of Science and Technology of China ) and Yiyun Chen ( University of Science and Technology of China ).
Constructing Program Invariants via Solving QBF
Shikun Chen ( National University of Defence Technology), Zhoujun Li ( Beihang University ) and Mengjun Li ( National University of Defence Technology).
12:10-14:00: Lunch
14:00-15:15: Session 8 : Concurrency (Chair: Gwan-Hwan Hwang)
Using Architectural Constraints for Deadlock-Freedom of Component Systems with Multiway Cooperation
Moritz Martens ( University of Mannheim ) and Mila Majster-Cederbaum ( University of Mannheim ).
Formal Reasoning about Concurrent Assembly Code with Reentrant Locks
Ming Fu ( University of Science and Technology of China ), Yu Zhang ( University of Science and Technology of China ) and Yong Li ( University of Science and Technology of China ).
Algorithms for Computing Weak Bisimulation Equivalence
Weisong Li ( Institute of Software , Chinese Academy of Sciences).
15:15-15:45: Coffee Break
15:45-17:25: Session 9 : Software Testing II (Chair: Hong Zhu)
Interpreting a successful testing process: risk and actual coverage
Marielle Stoelinga ( University of Twente ) and Mark Timmer ( University of Twente ).
Automated Test Case Generation based on Coverage Analysis
Tim A. Majchrzak ( University of Muenster ) and Herbert Kuchen ( University of Muenster ).
Exploring Topological Structure of Boolean Expressions for Test Data Selection
Lian Yu ( Peking University ), Wei Zhao (IBM China Research Lab), Xiangdong Fan ( Peking University ) and Jun Zhu (IBM China Research Lab).
On Testing 1-Safe Petri Nets
Guy-Vincent Jourdan ( University of Ottawa ) and Gregor von Bochmann ( University of Ottawa ).
Annex A : Poster Session I (15:15-16:15, Day 1)
Verifying the Implementation of an Operating System Scheduler
Moritz Kleine (Technische Universität Berlin ), Björn Bartels (Technische Universität Berlin ), Thomas Göthel (Technische Universität Berlin ) and Sabine Glesner (Technische Universität Berlin ).
A Tool For Estimating Memory Usage
Shengyi Wang ( Peking University ) and Zongyan Qiu ( Peking University ).
A Framework for Dependency Evaluation of the Agent oriented Methodologies workflows
Tannaz Alinaghi ( University of Tehran ), Camellia Ghoroghi ( University of Tehran ), Ahmad Sabouri ( University of Tehran ), and Reza Basseda ( University of Tehran ).
Spontaneous Detection of Infinite Loops and Livelocks in Dynamic Testing of Concurrent Programs
Che-Sheng Lin ( National Taiwan Normal University ) and Gwan-Hwan Hwang ( National Taiwan Normal University ).
Specifying and verifying PLC Systems with TLA+
Hehua Zhang (Tsinghua university), Stephan Merz (INRIA Lorraine) and Ming Gu ( Tsinghua University ).
Domain Hierarchies: a Basic Theoretical Framework for Integrating Software Domains
Pierre Kelsen ( University of Luxembourg ) and Qin Ma ( University of Luxembourg ).
Improve Semantic Web Services Discovery through Similarity Search in Metric Space
Minghui WU (Zhejiang University), Fanwei ZHU (Zhejiang University), Jia LV (Zhejiang University), Tao Jiang (Zhejiang University) and Jing Ying (Zhejiang University).
Parameterized Bisimulation Infinite Evolution Mechanism
Yanfang Ma ( East China Normal University ), Min Zhang (East China Normal University), and Yixiang Chen ( East China Normal University ).
Formal Modeling MapReduce with CSP
Wen Su ( East China Normal University ), Fan Yang ( East China Normal University ), Huibiao Zhu ( East China Normal University ), and Qin Li ( East China Normal University).
Formal Specification and Experiments of an Expressive Human-Computer Ensemble System with Rehearsal
Tetsuya Mizutani ( University of Tsukuba ) , Tatsuo Suzuki ( University of Tsukuba ) , Masayuki Shio ( Tokiwa University ) and Yasuwo Ikeda ( Mejiro University ).
Towards Automated Software Verification Using Model Checking Techniques
Somayeh Asadollahi (Islamic Azad University of Malayer),Vahid Rafe (Islamic Azad University of Malayer ),Reza Rafeh (Islamic Azad University of Malayer) and Adel T. Rahmani ( Iran University of Science and Technology).
Annex B : Poster Session II (15:15-16:15, Day 2)
Data Structure Shape Inference and Verification for OO Programs
Rhys Owen (Wellington Institute of Technology) and Hugh Anderson (Wellington Institute of Technology).
DUMS: a Dynamical Updatable Monitoring System for Desktop PCs used for Distributed Computing
Jinwei Wang ( Tianjin Normal University ), Huazhi Sun ( Tianjin Normal University ) and Jianping Fan ( Tianjin Normal University ).
Formal Representation and Analysis of a Near Miss Accident in N\Sigma-labeled Calculus
Tetsuya Mizutani ( University of Tsukuba ) , Shigeru Igarashi ( University of Tsukuba ) , Yasuwo Ikeda ( Mejiro University ) and Masayuki Shio ( Tokiwa University ).
Representing Aspects in Design
Saqib Iqbal ( Univeristy of Huddersfield ) and Gary Allen ( Univeristy of Huddersfield ).
G-BLAST: BLAST manager in an heterogeneous distributed environment
Dong-Wook Kim (Mokpo National University), Tae-Sung Jung (Korea Research Institute of Bioscience and Biotechnology), Dae-Won Kim (Korea Research Institute of Bioscience and Biotechnology), Seong-Hyeuk Nam (Korea Research Institute of Bioscience and Biotechnology), Hyuk-Ryul Kwon (Korea Research Institute of Bioscience and Biotechnology), Sang-Haeng Choi (Korea Research Institute of Bioscience and Biotechnology) , Han-Suk Choi (Mokpo National University) and Hong-Seog Park (Korea Research Institute of Bioscience and Biotechnology).
Probabilistic Coordination Language for Component Dynamic Composition
Dehui Du ( East China Normal University ).
Modeling Fault Tolerant Services in Service-Oriented Architecture
Farzaneh Mahdian (Islamic Azad University of Tooyserkan),Vahid Rafe (Islamic Azad University of Malayer ), Reza Rafeh (Islamic Azad University of Malayer) and Adel T. Rahmani ( Iran University of Science and Technology).
Heap Memory Requirements analysis via Separation Logic
Guanhua He ( Durham University ) and Chenguang Luo ( Durham University ).
Automated Verification Using Unified Control Flows
Cristian Gherghina ( National University of Singapore ) and Cristina David (National University of Singapore ).
MARS: Metamodel Recovery from Multi-Tiered Models Using Grammar Inference
Qichao Liu ( University of Alabama at Birmingham ), Faizan Javed (Regions Financial Corp), Marjan Mernik ( University of Alabama at Birmingham ), Barrett R. Bryant ( University of Alabama at Birmingham ), Jeff Gray ( University of Alabama at Birmingham ), Alan Sprague ( University of Alabama at Birmingham ), and Dejan Hrncic ( University of Maribor ).
Formal Approaches to Deadlock Analysis in Competitions of Shared Web Resources
Jieqi Ding ( East China Normal University ), Han Zhu ( East China Normal University ), Huibiao Zhu ( East China Normal University ), and Qin Li ( East China Normal University).
Measuring the Survivability of Object-Oriented Software
Jueliang Hu ( East China Normal University ), Zuohua Ding (East China Normal University), and Jing Liu ( East China Normal University ).
| 