Leveraging Applications of Formal Methods, Verification and Validation : Third International Symposium, ISoLA 2008, Porto Sani, Greece, October 13-15, 2008, Proceedings

This book constitutes the thoroughly refereed proceedings of the Third International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, held in Porto Sani, Greece, in October 2008 The 68 revised full papers presented together with 2 invited talks and 1 keynote speech were carefully selected from numerous submissions. The topics covered are tools and applications in industrial software quality control; an introduction of multi-core systems in automotive applications; model-driven SOA; applications of formal approaches to service-oriented computing; trustworthy computing: theories, methods, tools and experience in China and South East Asia; non-functional requirements in embedded systems; processes, methods and tools for developing educational modules to support teaching and technology transfer; ubiquitous and context aware systems; formal methods for analysing and verifying very large systems; tools for service-oriented discovery of knowledge; tackling the challenges of software development process for SMEs with rigorous support and open source. Front Matter....Pages - Architecture Based Specification and Verification of Embedded Software Systems (Work in Progress)....Pages 1-13 Information System Engineering Supporting Observation, Orientation, Decision, and Compliant Action....Pages 14-14 Modelling Coordination and Compensation....Pages 15-36 Animating Event B Models by Formal Data Models....Pages 37-55 Automated Formal Testing of C API Using T2C Framework....Pages 56-70 Tailoring and Optimising Software for Automotive Multicore Systems....Pages 71-81 Fault Handling Approaches on Dual-Core Microcontrollers in Safety-Critical Automotive Applications....Pages 82-92 Timing Validation of Automotive Software....Pages 93-107 Towards Using Reo for Compliance-Aware Business Process Modeling....Pages 108-123 On the Risk Management and Auditing of SOA Based Business Processes....Pages 124-138 SCA and jABC: Bringing a Service-Oriented Paradigm to Web-Service Construction....Pages 139-154 A Use-Case Driven Approach to Formal Service-Oriented Modelling....Pages 155-169 Sensoria Patterns: Augmenting Service Engineering with Formal Analysis, Transformation and Dynamicity....Pages 170-190 Safety and Response-Time Analysis of an Automotive Accident Assistance Service....Pages 191-205 A Framework for Analyzing and Testing the Performance of Software Services....Pages 206-220 A Framework for Contract-Policy Matching Based on Symbolic Simulations for Securing Mobile Device Application....Pages 221-236 ASERE : Assuring the Satisfiability of Sequential Extended Regular Expressions....Pages 237-251 Computing Must and May Alias to Detect Null Pointer Dereference....Pages 252-261 A Partial Order Reduction Technique for Parallel Timed Automaton Model Checking....Pages 262-276 Program Verification by Reduction to Semi-algebraic Systems Solving....Pages 277-291 Debugging Statecharts Via Model-Code Traceability....Pages 292-306 Model Checking CSP Revisited: Introducing a Process Analysis Toolkit....Pages 307-322 Formal Use of Design Patterns and Refactoring....Pages 323-338 A Component-Based Access Control Monitor....Pages 339-353 Navigating the Requirements Jungle....Pages 354-368 Non-functional Avionics Requirements....Pages 369-384 A Simulation Approach for Performance Validation during Embedded Systems Design....Pages 385-399 Optimizing Automatic Deployment Using Non-functional Requirement Annotations....Pages 400-414 Experiences with Evolutionary Timing Test of Automotive Software Components....Pages 415-429 Measurement-Based Timing Analysis....Pages 430-444 ALL-TIMES – A European Project on Integrating Timing Technology....Pages 445-459 Weaving a Formal Methods Education with Problem-Based Learning....Pages 460-472 Encouraging the Uptake of Formal Methods Training in an Industrial Context....Pages 473-477 Computer-Supported Collaborative Learning with Mind-Maps....Pages 478-489 Agile IT: Thinking in User-Centric Models....Pages 490-502 Specialization and Instantiation Aspects of a Standard Process for Developing Educational Modules....Pages 503-518 A Formal Framework for Modeling Context-Aware Behavior in Ubiquitous Computing....Pages 519-533 Contexts and Context Awareness in View of the Diagram Predicate Framework....Pages 534-547 The Use of Adaptive Semantic Hypermedia for Ubiquitous Collaboration Systems....Pages 548-560 The Use of Formal Ontology to Specify Context in Ubiquitous Computing....Pages 561-571 High Service Availability in MaTRICS for the OCS....Pages 572-586 Supporting Requirements Definition and Quality Assurance in Ubiquitous Software Project....Pages 587-603 Squeeze All the Power Out of Your Hardware to Verify Your Software!....Pages 604-618 Static Partial-Order Reduction of Concurrent Systems in Polynomial Time....Pages 619-633 An Extensible Space-Based Coordination Approach for Modeling Complex Patterns in Large Systems,....Pages 634-648 On the Design of Knowledge Discovery Services Design Patterns and Their Application in a Use Case Implementation....Pages 649-662 The ASK System and the Challenge of Distributed Knowledge Discovery....Pages 663-668 A Scenario Implementation in R for SubtypeDiscovery Examplified on Chemoinformatics Data....Pages 669-683 Requirements for Ontology Based Design Project Assessment....Pages 684-692 Organizing the World’s Machine Learning Information....Pages 693-708 Workflow Testing....Pages 709-723 The jABC Approach to Rigorous Collaborative Development of SCM Applications....Pages 724-737 Gesper: Support to Capitalize on Experience in a Network of SMEs....Pages 738-752 Directed Generation of Test Data for Static Semantics Checker....Pages 753-768 Event-Based Approach to Modelling Dynamic Architecture: Application to Mobile Ad-Hoc Network....Pages 769-781 Trusted Theorem Proving: A Case Study in SLD-Resolution....Pages 782-796 High Level Analysis, Design and Validation of Distributed Mobile Systems with CoreASM ....Pages 797-814 Optimizing the System Observability Level for Diagnosability....Pages 815-830 Weaving Authentication and Authorization Requirements into the Functional Model of a System Using Z Promotion....Pages 831-846 Simple Gedanken Experiments in Leveraging Applications of Formal Methods....Pages 847-861 Composition of Web Services Using Wrappers....Pages 862-865 Back Matter....Pages - This volume contains the conference proceedings of ISoLA 2008, the Third International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, which was held in Porto Sani (Kassandra, Chalkidiki), Greece during October 13–15, 2008, sponsored by EASST and in cooperation with the IEEE Technical Committee on Complex Systems. Following the tradition of its forerunners in 2004 and 2006 in Cyprus, and the ISoLA Workshops in Greenbelt (USA) in 2005 and in Poitiers (France) in 2007, ISoLA 2008 provided a forum for developers, users, and researchers to discuss issues related to the adoption and use of rigorous tools and methods for the specification, analysis, verification, certification, construction, test, and maintenance of systems from the point of view of their different application domains. Thus, the ISoLA series of events serves the purpose of bridging the gap between designers and developers of rigorous tools, and users in engineering and in other disciplines, and to foster and exploit synergetic relationships among scientists, engineers, software developers, decision makers, and other critical thinkers in companies and organizations. In p- ticular, by providing a venue for the discussion of common problems, requirements, algorithms, methodologies, and practices, ISoLA aims at supporting researchers in their quest to improve the utility, reliability, flexibility, and efficiency of tools for building systems, and users in their search for adequate solutions to their problems. Constitutes the refereed proceedings of the Third International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, held in Porto Sani, Greece, in October 2008. This book covers tools and applications in industrial software quality control.