Table of Contents

• Triumphs and Challenges for Model-Oriented Formal Methods: The VDM:::++::: Experience (Abstract)John S. Fitzgerald, Peter Gorm Larsen. 1-4 [doi]
• Formal Security Analysis in Industry, at the Example of Electronic Distribution of Aircraft Software (EDS)David von Oheimb. 5 [doi]
• Certificates of Resource Usage on Mobile TelephonesThomas Jensen. 6-7 [doi]
• Program Safety via Programmer SafetyJoseph Kiniry. 8 [doi]
• The AUTOSAR Timing Model - Status and Challenges -Kai Richter. 9-10 [doi]
• Analysis Techniques for Service ModelsWolfgang Reisig, Dirk Fahland, Niels Lohmann, Peter Massuthe, Christian Stahl, Daniela Weinberg, Karsten Wolf, Kathrin Kaschner. 11-17 [doi]
• Software Assurance Research Infusion: The NASA ExperienceMichael G. Hinchey, Thomas Pressburger, Martin S. Feather, Lawrence Markosian, Wes Deadrick. 18-27 [doi]
• Verifying LTL Properties on Hierarchical Systems: Application to Aircraft AutopilotMohammed Al Achhab, Ahmed Hammad, Hassan Mountassir. 28-35 [doi]
• Formal Modelling of Avionics Systems. An Approach Based on Category Theory and the EXPRESS Modelling LanguageYamine Aït Ameur, Remi Delmas, Alexandre Cortier, Virginie Wiels. 36-44 [doi]
• Reasoning about Airport Security Regulations Using the Focal EnvironmentDavid Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge. 45-52 [doi]
• Concurrent Testing of Java Components Using Java PathFinderVadim Mutilin. 53-59 [doi]
• The UniTESK Approach to Specification-Based Validation of Hardware DesignsAlexander Kamkin. 60-66 [doi]
• Combining Logic and Algebraic Techniques for Program Verification in TheoremaLaura Kovács, Nikolaj Popov, Tudor Jebelean. 67-74 [doi]
• Automatic Test Generation for Model-Based Code GeneratorsSergey V. Zelenov, Denis V. Silakov, Alexander K. Petrenko, Mirko Conrad, Ines Fey. 75-81 [doi]
• Retrenching the Purse: Hashing Injective CLEAR Codes, and Security PropertiesRichard Banach, Michael Poppleton, Czeslaw Jeske, Susan Stepney. 82-90 [doi]
• Formal Modelling of Dynamic Coalitions, with an Application in Chemical EngineeringJeremy Bryans, John S. Fitzgerald, Cliff B. Jones, Igor Mozolevsky. 91-98 [doi]
• CARVER: A Slicing Tool for Communicating Automata SpecificationsSébastien Labbé, Arnault Lapitre. 99-102 [doi]
• Model-Based Development of Fault-Tolerant Embedded SoftwareChristian Buckl, Alois Knoll, Gerhard Schrott. 103-110 [doi]
• A Formal Specification of a Programming Language: Design of PitLeif Pedersen, Hassan Reza. 111-118 [doi]
• Intransitive Noninterference in Dependence GraphsChristian Hammer, Jens Krinke, Frank Nodes. 119-128 [doi]
• Formally Proved Anti-tearing Properties of Embedded C CodeJune Andronick. 129-136 [doi]
• Kiasan: A Verification and Test-Case Generation Framework for Java Based on Symbolic ExecutionXianghua Deng, Robby, John Hatcliff. 137 [doi]
• Extending Source Code Generators for Evidence-Based Software CertificationEwen Denney, Bernd Fischer. 138-145 [doi]
• Application of Bioinformatics in the Design of Gene Expression MicroarraysSabah Khalid, Mohsin Khan, Ping Wang, Xiaohui Liu, Suling Li. 146-160 [doi]
• A Novel Method for Obtaining Real Time Control Strategy Using GA for Dynamical Systems Subjected to External Arbitrary ExcitationsM. Saud, I. I. Esat. 161-168 [doi]
• Real-Coded Quantum Inspired Evolution Algorithm Applied to Engineering Optimization ProblemsF. S. Alfares, I. I. Esat. 169-176 [doi]
• Safety and Dependability Analysis of Self-Adaptive SystemsMatthias Güdemann, Frank Ortmeier, Wolfgang Reif. 177-184 [doi]
• Organic Computing - Addressing Complexity by Controlled Self-OrganizationJürgen Branke, Moez Mnif, Christian Müller-Schloer, Holger Prothmann, Urban Richter, Fabian Rochner, Hartmut Schmeck. 185-191 [doi]
• Real-Time Property Verification in Organic Computing SystemsSteffen Stein, Arne Hamann, Rolf Ernst. 192-197 [doi]
• Recognizing Traffic Jams with Hovering Data CloudsSándor P. Fekete, Christiane Schmidt, Axel Wegener, Stefan Fischer. 198-203 [doi]
• Cost-Efficient Worst-Case Execution Time Analysis in Industrial PracticeJan Staschulat, Jörn-Christian Braam, Rolf Ernst, Thomas Rambow, Rainer Schlör, Rainer Busch. 204-211 [doi]
• Static WCET Analysis of Real-Time Task-Oriented Code in Vehicle Control SystemsDaniel Sehlberg, Andreas Ermedahl, Jan Gustafsson, Björn Lisper, Steffen Wiegratz. 212-219 [doi]
• Towards an Integration of Low-Level Timing Analysis and Model-Based Code GenerationChristian Ferdinand, Reinhold Heckmann, Hans-Jörg Wolff, Christian Renz, Manabendra Gupta, Oleg Parshin. 220-226 [doi]
• Challenges of Timing Verification Tools in the Automotive DomainPascal Montag, Steffen Görzig, Paul Levi. 227-232 [doi]
• The Worst Case Execution Time Tool Challenge 2006Jan Gustafsson. 233-240 [doi]
• The Worst Case Execution Time Tool Challenge 2006: The External TestLili Tan. 241-248 [doi]
• Model Checking Techniques for the Performance Analysis of Delay Tolerant Networks with On-off BehaviorMichele Garetto, Marco Gribaudo. 249-254 [doi]
• Model Checking Medium Access Control for Sensor NetworksPaolo Ballarini, Alice Miller. 255-262 [doi]
• Formal Techniques for the Analysis of Wireless NetworksA. K. McIver, Ansgar Fehnker. 263-270 [doi]
• Modeling of Sensor Networks Using XRMAkim Demaille, Sylvain Peyronnet, Benoît Sigoure. 271-276 [doi]
• "Towards a Trusted Compiler for a Query Language for Wireless Sensor Networks."T. E. Daniel, S. N. I. Mount, Robert M. Newman, Elena I. Gaura. 277-282 [doi]
• A Space and Time Requirements Logic for Sensor NetworksRachel Cardell-Oliver, Mark Reynolds, Mark Kranz. 283-289 [doi]
• Probabilistic Model Checking of Contention Resolution in the IEEE 802.15.4 Low-Rate Wireless Personal Area Network ProtocolMatthias Fruth. 290-297 [doi]
• Formal Executable Models of Cell Signaling PrimitivesCarolyn L. Talcott. 298-302 [doi]
• Biological LC/MS Preprocessing and Analysis with jABC, jETI and xcmsChristian Kubczak, Tiziana Margaria, Arno Fritsch, Bernhard Steffen. 303-308 [doi]
• Foundations for Web Services Orchestrations: Functional and QoS Aspects, JointlySidney Rosario, Albert Benveniste, Stefan Haar, Claude Jard. 309-316 [doi]
• Service Based Enabling Service Availability in the MaTRICS: A Model-Driven ApproachMarkus Bajohr, Tiziana Margaria, Bernhard Steffen. 317-324 [doi]
• Web Services for the Integration of XML-Based Content into Learning Platforms: A Three-level ModelReinhold Kröger, Ulrike Lucke, Markus Schmid, Djamshid Tavangarian. 325-331 [doi]
• Semi-automated Workflow SynthesisAbílio Fernandes, Karin Koogan Breitman, Tatiana Almeida S. C. Vieira, Marco A. Casanova, Antonio L. Furtado. 332-334 [doi]
• Context Awareness Systems Design and ReasoningJin Song Dong, Yuzhang Feng, Jing Sun, Jun Sun 0001. 335-340 [doi]
• REDLIB for the Formal Verification of Embedded SystemsFarn Wang. 341-346 [doi]
• Synthesis and Traceability of Scenario-Based Executable ModelsAnkit Goel, Abhik Roychoudhury. 347-354 [doi]
• Towards a Framework for Scalable Model Checking of Concurrent C ProgramsJi Wang, Xiaodong Yi, Xuejun Yang. 355-362 [doi]
• Patterns with Algebraic Properties in BPEL0Geguang Pu, Huibiao Zhu, Jifeng He, Zongyan Qiu, Hongli Yang, Xiangpeng Zhao. 363-370 [doi]
• Harnessing Theories for Tool SupportZhiming Liu, Vladimir Mencl, Anders P. Ravn, Lu Yang. 371-382 [doi]
• Connecting Algebraic and Logical Descriptions of Concurrent SystemsNaijun Zhan. 383-391 [doi]
• Improve Model Checking Efficiency Using Specific Knowledge about the SystemJianhua Zhao, Bin Lei, Xuandong Li, Guoliang Zheng. 392-396 [doi]
• An SDL Implementation of the UMTS Radio Resource Control Protocol Oriented to Conformance TestingJosé M. Alvarez, Pedro de la Cámara, Jesús Martínez, Pedro Merino, Francisco C. Perez, Victoria Morillo. 397-401 [doi]
• The FMICS-jETI Platform: Status and PerspectivesTiziana Margaria, Christian Kubczak, Bernhard Steffen, Stefan Naujokat. 402-407 [doi]
• Verification in the Large via Symbolic ApproximationPeter T. Breuer, Simon Pickin. 408-415 [doi]
• Implementing Influence Analysis Using Parameterised Boolean Equation SystemsMaría-del-Mar Gallardo, Christophe Joubert, Pedro Merino. 416-424 [doi]
• Formal Verification of Consistency in Model-Driven Development of Distributed Communicating Systems and Communication ProtocolsDubravka Ilic, Elena Troubitsyna, Linas Laibinis, Sari Leppänen. 425-432 [doi]
• Comparative Analysis of Tools for Automated Software Re-engineering PurposesChristian Wagner, Tiziana Margaria, Hans-Georg Pagendarm. 433-440 [doi]
• A Formal Behavioral Semantics for TestMLJürgen Grossmann, Wolfgang Müller. 441-448 [doi]
• An Automated Approach for Writing Alloy Specifications Using InstancesSarfraz Khurshid, Muhammad Zubair Malik, Engin Uzuncaova. 449-457 [doi]
• Noise Makers Need to Know Where to be Silent - Producing Schedules That Find BugsYosi Ben-Asher, Eitan Farchi, Yaniv Eytani, Shmuel Ur. 458-465 [doi]
• [mc]square: A Model Checker for Microcontroller CodeBastian Schlich, Stefan Kowalewski. 466-473 [doi]