Table of Contents

• SFI: A Refinement Based Layered Software ArchitectureRalph-Johan Back. 1-2 [doi]
• Developing Quality Software Systems Using the SOFL Formal Engineering MethodShaoying Liu. 3-19 [doi]
• Maintaining Referential Integrity on the WebMark A. Hale. 20-21 [doi]
• Formal Methods in Enterprise ComputingRichard Jüllig. 22-23 [doi]
• Unifying Theories of Parallel ProgrammingJim Woodcock, Arthur P. Hughes. 24-37 [doi]
• ABC/ADL: An ADL Supporting Component CompositionHong Mei, Feng Chen, Qianxiang Wang, Yao-Dong Feng. 38-47 [doi]
• The Description of CORBA Objects Based on Petri NetsHong Zheng, Shi-xian Li. 48-56 [doi]
• Toward a Formal Model of Software ComponentsMaritta Heisel, Thomas Santen, Jeanine Souquières. 57-68 [doi]
• A Specification-Based Software Construction Framework for ReuseJing Liu, Huaikou Miao, Xiaolei Gao. 69-79 [doi]
• Specifying a Component Model for Building Dynamically Reconfigurable Distributed SystemsXuejun Chen. 80-91 [doi]
• Three-Tiered Specification of Micro-architecturesVangalur S. Alagar, Ralf Lämmel. 92-97 [doi]
• Modeling the Architecture for Component-Based E-commerce SystemJiayue Chang, Huadong Ma. 98-102 [doi]
• Component Specification and Wrapper/Glue Code Generation with Two-Level Grammar Using Domain Specific KnowledgeFei Cao, Barrett R. Bryant, Rajeev R. Raje, Mikhail Auguston, Andrew M. Olson, Carol C. Burt. 103-107 [doi]
• Abstract Specification in Object-Z and CSPGraeme Smith, John Derrick. 108-119 [doi]
• Mechanization of an Integrated Approach: Shallow Embedding into SAL/PVSChristian Attiogbé. 120-131 [doi]
• Concept Use or Concept Refinement: An Important Distinction in Building Generic SpecificationsDavid R. Musser, Zhiqing Shao. 132-143 [doi]
• An Overview of Mobile Object-ZKenji Taguchi, Jin Song Dong. 144-155 [doi]
• Z Approach to Semantic WebJin Song Dong, Jing Sun, Hai H. Wang. 156-167 [doi]
• Hardware/Software Partitioning in VerilogShengchao Qin, Jifeng He, Zongyan Qiu, Naixiao Zhang. 168-179 [doi]
• A Formal Methodology to Specify E-commerce SystemsAdriano M. Pereira, Mark A. J. Song, Gustavo Gorgulho, Wagner Meira Jr., Sérgio Vale Aguiar Campos. 180-191 [doi]
• Model-Based Specification Animation Using TestgraphsTim Miller, Paul A. Strooper. 192-203 [doi]
• An Abstract Model for Scheduling Real-Time ProgramsAlvaro E. Arenas. 204-215 [doi]
• A Specification and Validation Technique Based on STATEMATE and FNLOGOlfa Mosbahi, Leila Jemni Ben Ayed, Samir Ben Ahmed, Jacques Jaray. 216-220 [doi]
• Formal Representation and Analysis of Batch Stock Trading Systems by Logical Petri Net WorkflowsYuyue Du, Changjun Jiang. 221-225 [doi]
• A Calculus for Mobile Network SystemsJinfeng Huang, Ad Verschueren, Henri Aalderink, Johan J. Lukkien. 226-230 [doi]
• Modelling Real-Time Systems with Continuous-Time Temporal LogicGuangyuan Li, Zhisong Tang. 231-236 [doi]
• On Concept-Based Definition of Domain-Specific LanguagesYing Liu, Naixiao Zhang. 237-248 [doi]
• Formal Specification of Evolutionary Software AgentsHong Zhu. 249-261 [doi]
• Detecting Deadlock in Ada Rendezvous Flow Structure Based on Process AlgebraYuan Liu, Baowen Xu, Zhenqiang Chen. 262-274 [doi]
• Formal Analysis of Real-Time Systems with SAMHuiqun Yu, Xudong He, Yi Deng, Lian Mo. 275-286 [doi]
• Tool Support for Visualizing CSP in UMLMuan Yong Ng, Michael J. Butler. 287-298 [doi]
• Theorem Prover Support for Precondition and Correctness CalculationOrieta Celiku, Joakim von Wright. 299-310 [doi]
• XML-Based Static Type Checking and Dynamic Visualization for TCOZJin Song Dong, Yuan-Fang Li, Jing Sun, Jun Sun 0001, Hai H. Wang. 311-322 [doi]
• µ-Chart-Based Specification and RefinementDoug Goldson, Greg Reeve, Steve Reeves. 323-334 [doi]
• Towards a Refinement Calculus for Concurrent Real-Time ProgramsSibylle Peuker, Ian J. Hayes. 335-346 [doi]
• Refinement Algebra for Formal Bytecode GenerationAdolfo Duran, Ana Cavalcanti, Augusto Sampaio. 347-358 [doi]
• Formal Modelling of Java GUI Event HandlingJessica Chen. 359-370 [doi]
• A New Algorithm for Service Interaction DetectionAna R. Cavalli, Stéphane Maag. 371-382 [doi]
• Specification of an Asynchronous On-chip BusJuha Plosila, Tiberiu Seceleanu. 383-395 [doi]
• Analysis of a Security Protocol in µCRLJun Pang. 396-400 [doi]
• Developing a Spell-Checker for Tajik Using RAISEGafurov Davrondjon, Tomasz Janowski. 401-405 [doi]
• M2Z: A Tool for Translating a Natural Language Software Specification into ZZarina Shukur, Abdullah Mohd Zin, Ainita Ban. 406-410 [doi]
• Abstract Interpretation with a Theorem ProverHugh Anderson. 411-422 [doi]
• Formal Reasoning about Hardware and Software Memory ModelsAbhik Roychoudhury. 423-434 [doi]
• Slicing Hierarchical Automata for Model Checking UML StatechartsJi Wang, Wei Dong, Zhichang Qi. 435-446 [doi]
• Formal Verification of a SONET Telecom System BlockM. Hasan Zobair, Sofiène Tahar. 447-458 [doi]
• Enabling Hardware Verification through Design ChangesAmr T. Abdel-Hamid, Sofiène Tahar, John Harrison. 459-470 [doi]
• Specification-Based Test Generation for Security-Critical Systems Using MutationsGuido Wimmel, Jan Jürjens. 471-482 [doi]
• A Formal Definition of Function Points for Automated Measurement of B SpecificationsHassan B. Diab, Marc Frappier, Richard St.-Denis. 483-494 [doi]
• Machine Code Type SafetyFan Guo, Yiyun Chen, RongGui Hu. 495-499 [doi]
• On the Formalized Semantics of Static Modeling Elements in UMLYan-Bing Jiang, Wei-Zhong Shao, Zhi-Yi Ma, Yao-Dong Feng. 500-510 [doi]
• From a B Specification to UML StateChart DiagramsAhmed Hammad, Bruno Tatibouët, Jean-Christophe Voisinet, Weiping Wu. 511-522 [doi]
• Formalizing UML Models with Object-ZHuaikou Miao, Ling Liu, Li Li. 523-534 [doi]
• Using Transition Systems to Unify UML ModelsZhiming Liu, Xiaoshan Li, Jifeng He. 535-547 [doi]
• A Formal Metamodeling Approach to a Transformation between the UML State Machine and Object-ZSoon-Kyeong Kim, David A. Carrington. 548-560 [doi]
• A UML Approach to the Design of Open Distributed SystemsBehzad Bordbar, John Derrick, A. Gill Waters. 561-572 [doi]
• A Semantic Model of Real-Time UMLSubash Shankar. 573-577 [doi]
• Research on Ontology-Oriented Domain Analysis on MISZhong Ming, Shi-xian Li, Xiu-rong Fang. 578-582 [doi]
• A Requirements Description Model Based on Conditional Directed GraphsZaobin Gan, Chuanbo Chen, Xiandeng Pei. 583-587 [doi]
• Introducing Reference Semantics via RefinementGraeme Smith. 588-599 [doi]
• Soundness, Completeness and Non-redundancy of Operational Semantics for Verilog Based on Denotational SemanticsHuibiao Zhu, Jonathan P. Bowen, Jifeng He. 600-612 [doi]
• Towards a Time Model for CircusAdnan Sherif, Jifeng He. 613-624 [doi]