Day 1: 17 April 2007 8:00-8:30 Registration 8:30-8:50 Opening 8:50-9:50 Invited Speaker: James C. Browne, The University of Texas at Austin 9:50-10:00 Break 10:00-10:25 52: Harald Fecher and Immo Grabe. Finite Abstract Models for Deterministic Transition Systems: Fair Parallel Composition and Refinement-Preserving Logic 10:25-10:50 73: Ingo Brückner, Klaus Dräger, Bernd Finkbeiner and Heike Wehrheim. Slicing Abstractions 10:50-11:05 59: Jin Yi and Wenhui Zhang. Efficient State Space Reduction For Automata By Fair Simulation 11:05-11:20 54: Domenico Bianculli, Paola Spoletini, Angelo Morzenti, Matteo Pradella and Pierluigi San Pietro. Model checking temporal metric specifications with Trio2Promela 11:20-11:30 Break 11:30-12:30 Poster Papers (See below for the list) 12:30-14:00 Lunch Break 14:00-15:00 Invited Speaker: Masahiro Fujita, The University of Tokyo 15:00-15:25 53: Mohammad Torabi Dashti, Srijith Krishnan Nair and Hugo L. Jonker. Nuovo DRM Paradiso: Towards a Verified Fair DRM Scheme 15:25-15:50 78: Mahdi Niamanesh and Rasool Jalili. Formalizing Compatibility and Substitutability in Communication Protocols Using I/O-Constraint Automata 15:50-16:10 Break 16:10-16:25 84: Mahdi Niamanesh, Sirwah Sabetghadam, Reza YousefZade Rahaghi and Rasool Jalili. Design and Implementation of a Dynamic-Reconfigurable Architecture for Protocol Stack 16:25-16:40 46: Mohammad Ebrahim Rafiei, Mohsen Taherian, Hamid Mousavi, Ali Movaghar and Rasool Jalili. Vulnerability Analysis in VGBPS using Prolog 16:40-17:05 64: Gizela Jakubowska and Wojciech Penczek. Is Your Security Protocol on Time? Day 2: 18 April 2007 9:00-10:00 Invited Speaker: Davide Sangiorgi, University of Bologna 10:00-10:25 11: Wan Fokkink, Allard Kakebeen and Jun Pang. Adapting the UPPAAL Model of a Distributed Lift System 10:25-10:50 83: Parosh Abdulla, Karin Quaas , James Worrell and Joel Ouaknine. Zone-Based Universality Analysis for Timed Automata 10:50-11:20 Break 11:20-11:45 33: Niloofar Razavi and Marjan Sirjani. Compositional Semantics of System-Level Designs Written in SystemC 11:45-12:00 51: Bahman Pourvatan and Nima Rouhy. An Alternative Algorithm for Constraint Automata Product 12:00-14:00 Lunch Break 14:00-14:25 22: Ramin Tavakoli Kolagari and Mark-Oliver Reiser. Reusing Requirements: The Need for Extended Variability Models 14:25-14:40 100: Mehran Sharafi, Fereidoon Shams Aliee and Ali Movaghar. Specifying Software Architectures Using Extended Automata-based Models 14:40-14:55 85: Saeed Parsa and Gholamreza Safi. ArchC#: A New Architecture Description Language for Distributed Systems 14:55-15:10 75: Matteo Baldoni, Guido Boella and Leendert van der Torre. Relationships Meet their Roles in Object Oriented Programming 15:10-15:40 Break 15:40-16:05 68: Marc Aiguier, Agnès Arnould, Pascale Le Gall and Delphine Longuet. Test selection criteria for quantifier-free first-order 16:05-16:30 76: Mercedes G. Merayo, Manuel Nunez and Ismael Rodríguez. Formal testing of systems presenting soft and hard deadlines   Social Event Day 3: 19 April 2007 9:00-10:00 Invited Speaker: Peter D. Mosses, Swansea University 10:00-10:25 38: Seyyed Vahid Hashemian and Farhad Mavaddat. Automatic Composition of Stateless Components: A Logical Reasoning Approach 10:25-10:50 36: Xin Chen, Jifeng He, Zhiming Liu and Naijun Zhan. A Model of Component-Based Programming 10:50-11:10 Break 11:10-11:35 62: Mario Bravetti and Gianluigi Zavattaro. Contract based Multi-party Service Composition 11:35-12:00 67: Alessandro Lapadula, Francesco Tiezzi and Rosario Pugliese. Regulating data exchange in service oriented applications 12:00-12:25 42: Filippo Bonchi, Antonio Brogi, Sara Corfini and Fabio Gadducci. A Behavioural Congruence for Web Services 12:25-14:00 Lunch Break 14:00-14:25 50: Carlo Montangero, Stephan Reiff-Marganiec and Laura Semini. Logic based detection of conflicts in Appel policies 14:25-14:50 71: Magnus O. Myreen, Anthony C. J. Fox and Michael J. C. Gordon. Hoare Logic for ARM Machine Code 14:50-15:15 29: Michel Reniers and Muck van Weerdenburg. Action Abstraction in Timed Process Algebra: The Case for an Untimed Silent Step 15:50-15:40 61: Michele Boreale and Lucia Acciai. Type Abstractions of Name-Passing Processes 15:40-16:00 Break 16:00-16:25 77: Mercedes G. Merayo, Manuel Nunez and Ismael Rodríguez. Formal specification of multi-agent systems by using EUSMs 16:25-16:50 18: Abdolmajid Mousavi, Behrouz Far, Armin Eberlein and Behrouz Heidari. Strong Safe Realizability of Message Sequence Chart Specifications 16:50-17:20 Break 17:20-17:40 Symposium Closing Poster Papers: 20: Reza Basseda, Mostafa Haghir Chehreghani, Fattaneh Taghiyareh. Modeling and Model checking an Agent-Based System Using Rebeca 23: Afsaneh Nassery, M.Reza Ghajar, Sara Najafzadeh, M.Amin Khajehnejad, Behjat Forouzandeh. Co-Design Partitioning Of G.729 Codec Using MATLAB 26: Ali Heydari, Mohammad Reza Jamali and Caro Lucas. Pattern Oriented Design of 3D Graphical Monitoring System 39: Maysam Yabandeh, Reza Shokri, and Nasser Yazdani. Formal Verification of CAR for Wireless Ad Hoc Networks 80: Azadeh Nematzadeh and Vahid Kazempour. Modeling Access Control at Architecture Level with UML 2.0 102: Behzad Moshiri, Farzad Arjmandi and Hamed Olfati. Gateways for Fieldbus Interoperations