Hardware supply-chain attacks are raising significant security threats to the boot process of multiprocessor systems. In this paper, we investigate critical stages of the multiprocessor system boot process and identify a new, prevalent hardware supply-chain attack surface that can bypass secure boot due to the absence of processor-authentication mechanisms. To defend against such attacks, in this paper, we present PA-Boot, the first formally verified processor-authentication protocol for secure boot in multiprocessor systems. PA-Boot is proved functionally correct and is guaranteed to detect multiple adversarial behaviors, such as processor replacements and man-in-the-middle attacks. The fine-grained formalization of PA-Boot and its fully mechanized security proofs are carried out in the Isabelle/HOL theorem prover with 348 lemmas/theorems and ~7,100 LoC. We further implement in C an instance of PA-Boot. Experiments on the proof-of-concept implementation indicate that PA-Boot can effectively identify boot-process attacks with a minor overhead (4.98% on Linux boot process) and thereby improve the security of multiprocessor systems.

Ensuring compliance with Information Flow Security (IFS) is known to be challenging, especially for concurrent systems with large codebases such as multicore operating system (OS) kernels. Refinement, which verifies that an implementation preserves certain properties of a more abstract specification, is promising for tackling such challenges. However, in terms of refinement-based verification of security properties, existing techniques are still restricted to sequential systems or lack the expressiveness needed to capture complex security policies for concurrent systems.

We present the first formal semantics for the Solana eBPF bytecode language used in smart contracts on the Solana blockchain platform. Our formalization accurately captures all binary-level instructions of the Solana eBPF instruction set architecture. This semantics is structured in a small-step style, facilitating the formalization of the Solana eBPF interpreter within Isabelle/HOL. We provide a semantics validation framework that extracts an executable semantics from our formalization to test against the original implementation of the Solana eBPF interpreter. This approach introduces a novel lightweight and non-invasive method to relax the limitations of the existing Isabelle/HOL extraction mechanism. Furthermore, we illustrate potential applications of our semantics in the formalization of the main components of the Solana eBPF virtual machine

ABSTRACT As the predominant standard for partitioning operating systems, ARINC 653 has been applied in many critical domains. However, its reliance on informal textual languages presents challenges for ensuring both the correctness of the standard itself and the conformity of a specification or an OS to this standard. This paper addresses the gap through formal work on the ARINC 653 standard. We provide a comprehensive formal specification of multi‐core ARINC 653 Part 1–5 using Isabelle/HOL that encompasses all the 68 services and covers all components outlined in the standard, then conduct a formal proof of conformity of the specification according to ARINC 653 Part 3A. Our work marks the first comprehensive multi‐core ARINC 653 specification with a formal conformity proof. Notably, we identify and address three defects in the standard document during the formal specification and proof.

Trusted Execution Environment (TEE) provides isolation for sensitive data in electronic devices and its compromise can lead to enormous losses. TEE's information-flow security is essential and can be robustly ensured by formal methods. Nevertheless, the cross-domain API invocation of TEE is intricate for information-flow analysis, and the service provider on the TEE, i.e., trusted application, brings complexity to the TEE specification and verification. Existing research seldom delves into general TEEs that are compliant with GlobalPlatform (GP), which is an important and universal TEE standard. Furthermore, they do not align with the requirements for Common Criteria certification. In this paper, we propose a TEE-applicable and Common Criteria-oriented framework to specify and verify the information-flow security of GP TEE, which is applied to the verification of the real-world commercial MiTEE. Firstly, we present a framework for TEE that aligns with the requirements of Common Criteria's highest assurance level (EAL 7). It incorporates a domainswitch based mechanism to model the cross-domain TEE API invocation and a parameterized modeling approach to handle trusted applications. Secondly, we model GlobalPlatform-compliant TEE with the framework as GP TEE security model layer and function layer, which are reusable for all GP TEEs. Thirdly, we specify MiTEE as the MiTEE design layer that refines GP TEE model. Lastly, we verify the information-flow security of GP TEE and MiTEE via theorem proving and uncover four critical vulnerabilities in MiTEE. This work contributes to MiTEE's acquirement of an EAL 5+ certificate. All works are carried out in Isabelle/HOL, with nearly 32000 lines of code.

Complex safety-critical systems require multiple models for a comprehensive description, resulting in error-prone development and laborious verification. Bidirectional transformation (BX) is an approach to automatically synchronizing these models. However, existing BX frameworks lack formal verification to enforce these models’ consistency rigorously. This paper introduces KBX, a formal bidirectional transformation framework for verified model synchronization. First, we present a matching logic-based BX model, providing a logical foundation for constructing BX definitions within the \(\mathbb{K}\) framework. Second, we propose algorithms to synthesize formal BX definitions from unidirectional ones, which allows developers to focus on crafting the unidirectional definitions while disregarding the reverse direction and missing information recovery for synchronization. Afterward, we harness \(\mathbb{K}\) to generate a formal synchronizer from the synthesized definitions for consistency maintenance and verification. To evaluate the effectiveness of KBX, we conduct a comparative analysis against existing BX frameworks. Furthermore, we demonstrate the application of KBX in constructing a BX between UML and HCSP for real-world scenarios, showcasing an 72% reduction in BX development effort compared to manual specification writing in \(\mathbb{K}\) .

Abstract The L4 API (Application Programming Interface) is a core component of the operating system, which serves as the interface between user-level processes and the microkernel, facilitating communication and interaction. It is crucial to ensure the correctness and reliability of the API. This paper proposes a comprehensive formal specification and verification for the L4 microkernel API. The specification is reusable for all implementations on architectures supported by the microkernel. To further improve reusability (e.g., for the L4 family), a parameterized model is abstracted, which mainly includes variables related to L4 components and safety properties built on them. The desired properties are composed of 350 functional correctness and 39 safety properties, where the safety properties cover existing invariants of the microkernel. Several rewriting rules and reasoning steps are proposed for verification to improve proof efficiency. The proofs of the specification w.r.t these properties are accomplished in the theorem prover Isabelle/HOL, and the results show that all definitions, lemmas, and proofs pass the prover’s check. During modeling and verification, 10 bugs in the source code are found, all of which are fixed in this paper.

The Trusted Execution Environment (TEE) plays a crucial role in modern computer systems and the compromise of TEE can result in enormous losses. Although numerous TEE products have been proposed, most of them lack robust security guarantees. To address this concern, GlobalPlatform (GP) defines the TEE security standard, Protection Profile (PP), which has gained widespread adoption in the TEE development and Common Criteria (CC) evaluation. However, despite its importance, GPTEE PP has never been formally specified and verified. In this paper, we present ProveriT , a parameterized, composable, and formally verified model of GPTEE PP. Firstly, we propose the first formal specification of GPTEE PP in a parameterized manner, encompassing the definition of security problems, security objectives, and security functional requirements. Secondly, we provide a compositional framework, utilizing horizontal calculus and vertical calculus, to flexibly combine specific security functional requirements for TEE developers and reduce proof efforts for verification. ProveriT is extensible and reusable for the verification and CC evaluation of specific TEE products. Thirdly, we conduct a comprehensive formal verification of rationales in the model to ensure the correctness of GPTEE PP. During the verification, 8 issues are discovered and we provide suggestions to resolve them. Finally, we demonstrate the extensibility and effectiveness of ProveriT by applying it to the verification of a commercial TEE. All the specifications and verification are carried out in the Isabelle/HOL theorem prover.

Virtual Private Cloud (VPC) has become a widely used cloud computing service, serving as a foundational web infrastructure for many organizations. Nevertheless, the growing problem of reachability issues poses significant threats to the security and reliability of VPC networks, potentially resulting in critical security concerns such as data breaches and service outages. Although there has been substantial progress in recent reachability analysis, existing methods lack validation of correctness. Moreover, current analyses are tailored for One-to-One reachability where both the source and the destination are fixed, and fail to efficiently answer One-to-Multi reachability queries, which involve computing all reachable destinations for a given source node. To address the above challenges, we propose VeriReach, the first formally verified algorithm that provides comprehensive and efficient reachability analysis in large-scale VPC networks. The reachability analysis result of VeriReach is proved to be equivalent to the original reachability semantics of the VPC networks, ensuring its correctness (i.e., soundness and completeness). The fine-grained formalization of VeriReach and its fully mechanized correctness proofs are carried out in Isabelle/HOL theorem prover with 282 lemmas/theorems and $\sim 4,900{\mathrm{LoC}}$. We further implement VeriReach in C++ and the evaluations indicate that VeriReach is more efficient and scalable than MonoSAT, the state-of-the-art SMT solver, when applied to large-scale VPC networks for reachability analysis.

As online coding technology advances, various related products are emerging, but we observe that there are not many examples of introducing online coding into the field of theorem proving. We introduce Isabelle/Cloud, an online coding platform and user environment for the Isabelle theorem proving assistant. The primary objective of Isabelle/Cloud is to cloudify Isabelle using online coding technology, thereby addressing the issue of loading large projects. Leveraging the understanding of the Isabelle architecture, we have modified, replaced, and added some modules, encapsulated the Isabelle environment using containers, and developed the front-end and back-end. As a cloud platform, Isabelle/Cloud enables users to create a complete Isabelle environment with different versions that are isolated from each other, while providing basic cloud coding and theorem proving services. The current version integrates most of the popular Isabelle libraries with excellent tutorials and cases, enabling users to directly create projects from the tutorial code for practical exercises. Evaluation of the platform shows that Isabelle/Cloud performs better when dealing with large projects. The new platform opens up new possibilities for interaction and presentation, and it is currently in use.

Trusted Execution Environments (TEEs) play a crucial role in embedded systems, IoT, and cloud computing. However, their security issues are a major concern, particularly related to defects or improper implementations in access control mechanisms. Such issues can result in severe problems like privilege escalation and unintended memory accesses during inter-domain communication. Moreover, employing mathematical methods for rigorous security guarantees is essential.To address these challenges, we propose Lark, a cross-domain access control for TEEs, which is modeled and verified in Isabelle/HOL. Lark applies orthogonal access control attributes on memory to decouple access permissions of different privilege levels. Additionally, it enforces strict access permission checks for inter-domain communications. For a strict security guarantee, Lark is formalized and verified in Isabelle/HOL, with 84 definitions and 35 lemmas containing ∼1,600 lines of code. The machine-checkable proofs demonstrate that Lark ensures memory isolation and information flow security. We identify and resolve an inter-domain communication issue within an open-source TEE, and develop a prototype that implements the access control features of Lark. Exhaustive evaluations on real-world applications demonstrate that Lark introduces less than 5% performance overhead.

ARINC 653 as the de facto standard of partitioning operating systems has been applied in many safety-critical domains. The multi-core version of ARINC 653, ARINC 653 Part 1-4 (Version 4), provides support for services to be utilized with a module that contains multiple processor cores. Formal specification and analysis of this standard document could provide a rigorous specification and uncover concealed errors in the textual description of service requirements. This article proposes a specification method for concurrency on a multi-core platform using Event-B, and a refinement structure for the complicated ARINC 653 Part 1-4 provides a comprehensive, stepwise refinement-based Event-B specification with seven refinement layers and then performs formal proof and analysis in RODIN. We verify that the errors discovered in the single-core version standard (ARINC 653 Part 1-3) also exist in the ARINC 653 Part 1-4 during the formal specification and analysis.

Sensitive resources in Trusted Execution Environment (TEE) have suffered serious security threats in recent years. Previous protection approaches either lack a strong assurance of TEE security properties or are limited to a single platform. We propose a compatible verified TEE architecture, calledCVTEE, which delegates a security monitor to manage TEE resources securely. This architecture has two key advantages: i) its functional correctness and security are guaranteed by a machine-checkable proof of security objectives of Trusted Application (TA) isolation, runtime confidentiality, and runtime integrity, and ii) it is applicable to different TEE platforms and implementation-independent due to its high level of abstraction and non-determinism of data types. Note that access control policy and information flow control policy are the core for security management of resources. After formally specifying the security attributes of TEE resources, we develop these policies based on Common Criteria (CC) in the security monitor and provide atomic interfaces.CVTEEis formally verified with 386 lemmas/theorems and$\sim$10,000 LOC of Isabelle/HOL. In addition, we implement a proof of concept for the access control module of Teaclave, and prove that the constructed access control model meets the security requirements through 5 theorems.

The challenge of requirements for the finer-grained isolated domain in Trusted Execution Environment (TEE) has been increasing, including the accuracy and security of resource management. However, the current access control mechanism for TEE cannot provide strict security assurances due to a lack of strict formal verification. In order to address the problem, in this paper, we first present the definition of multi-domain TEE, and propose a verified tag-based access control framework called REAL to provide the strict access control policy. We develop a high-level formal functional specification of REAL, and prove its correctness and security properties with 119 lemmas/theorems and ∼ 4,000 LOC of Isabelle/HOL. We also implement a page-level access control prototype called SOP-TEE and demonstrate that it correctly achieve the security objectives while merely incurring less than 0.3% overhead.

To make feasible and scalable the verification of large and complex concurrent systems, it is necessary the use of compositional techniques even at the highest abstraction layers. When focusing on the lowest software abstraction layers, such as the implementation or the machine code, the high level of detail of those layers makes the direct verification of properties very difficult and expensive. It is therefore essential to use techniques allowing to simplify the verification on these layers. One technique to tackle this challenge is top-down verification where by means of simulation properties verified on top layers (representing abstract specifications of a system) are propagated down to the lowest layers (that are an implementation of the top layers). There is no need to say that simulation of concurrent systems implies a greater level of complexity, and having compositional techniques to check simulation between layers is also desirable when seeking for both feasibility and scalability of the refinement verification. In this article, we present CSim 2 a (compositional) rely-guarantee-based framework for the top-down verification of complex concurrent systems in the Isabelle/HOL theorem prover. CSim 2 uses CSimpl, a language with a high degree of expressiveness designed for the specification of concurrent programs. Thanks to its expressibility, CSimpl is able to model many of the features found in real world programming languages like exceptions, assertions, and procedures. CSim 2 provides a framework for the verification of rely-guarantee properties to compositionally reason on CSimpl specifications. Focusing on top-down verification, CSim 2 provides a simulation-based framework for the preservation of CSimpl rely-guarantee properties from specifications to implementations. By using the simulation framework, properties proven on the top layers (abstract specifications) are compositionally propagated down to the lowest layers (source or machine code) in each concurrent component of the system. Finally, we show the usability of CSim 2 by running a case study over two CSimpl specifications of an Arinc-653 communication service. In this case study, we prove a complex property on a specification, and we use CSim 2 to preserve the property on lower abstraction layers.

Messaging system as a communicating infrastructure is a safety-critical component of autonomous vehicles. For the purpose of safety certification of Level 4 autonomous driving systems, its necessary to provide a formally verified specification of messaging systems. This paper presents a realistic case study using the PiCore rely-guarantee framework to formally verify the DGPS (Differential Global Positioning System) of UISEE autonomous driving systems. We first create an axiom model of messaging systems by extending PiCore, which is reusable for concrete applications. The model supports dynamic configuration of message buffers as well as the automatic generation of the rely and guarantee conditions for compositional reasoning. It is instantiated when developing the formal specification of DGPS. Then, we use the rely-guarantee proof system of PiCore to verify the functional correctness and invariant of DGPS. The specification and its proof provide a strong evidence for the ongoing safety certification of DGPS.

Formal verification of concurrent operating systems (OSs) is challenging, and in particular the verification of the dynamic memory management due to its complex data structures and allocation algorithm. Up to our knowledge, this paper presents the first formal specification and mechanized proof of a concurrent buddy memory allocation for a real-world OS. We develop a fine-grained formal specification of the buddy memory management in Zephyr RTOS. To ease validation of the specification and the source code, the provided specification closely follows the C code. Then, we use the rely-guarantee technique to conduct the compositional verification of functional correctness and invariant preservation. During the formal verification, we found three bugs in the C code of Zephyr.

Buddy memory allocation algorithms are widely adopted by various memory management systems for managing memory layouts. Rigorous mathematical proofs provide strong assurance to improve the confidence on the reliability of a memory management system. In this paper, we model and formally verify, in the interactive theorem prover Isabelle/HOL, a buddy memory allocation model, which preserves functional correctness and security properties. Firstly, we construct a specification consisting of operations to allocate and dispose memory blocks according to a buddy memory allocation algorithm. Then we verify that the specification preserves key invariants over the memory to guarantee functional correctness of the algorithm. Finally, we verify that the specification also preserves the integrity of the memory. Therefore, they do not affect other memory blocks previously allocated.

Bugs in memory management of Operating Systems may lead to crashing. This paper presents a case study of formal verification on the buddy memory allocation component of the Zephyr RTOS kernel. The algorithm of the component allows memory blocks of 4-power sizes to be dynamically allocated by efficiently partitioning larger blocks into smaller ones, and then be released supporting immediate and automatic combining of smaller blocks. The execution of memory allocation is preemptive, which means that the allocation may invoke rescheduling when there is no block available for memory requests. In this paper, we provide a fine-grained formal specification of buddy memory allocation and formally verify its safety via invariants and functional correctness. The specification covers all the elements of the data structure as well as all statements of memory initialization, allocation, and release presented in the C source code. During the formal verification, we found a functional flaw in the C code. To the best of our knowledge, this paper is the first effort of formal verification at a fine-grained level on buddy memory allocation in Operating Systems.

Assurance of information-flow security by formal methods is mandated in security certification of separation kernels. As an industrial standard for improving safety, ARINC 653 has been complied with by mainstream separation kernels. Due to the new trend of integrating safe and secure functionalities into one separation kernel, security analysis of ARINC 653 as well as a formal specification with security proofs are thus significant for the development and certification of ARINC 653 compliant Separation Kernels (ARINC SKs). This paper presents a specification development and security analysis method for ARINC SKs based on refinement. We propose a generic security model and a stepwise refinement framework. Two levels of functional specification are developed by the refinement. A major part of separation kernel requirements in ARINC 653 are modeled, such as kernel initialization, two-level scheduling, partition and process management, and inter-partition communication. The formal specification and its security proofs are carried out in the Isabelle/HOL theorem prover. We have reviewed the source code of one industrial and two open-source ARINC SK implementations, i.e., VxWorks 653, XtratuM, and POK, in accordance with the formal specification. During the verification and code review, six security flaws, which can cause information leakage, are found in the ARINC 653 standard and the implementations.

Partitioning operating systems (POSs) have been widely applied in safety-critical domains from aerospace to automotive. In order to improve the safety and the certification process of POSs, the ARINC 653 standard has been developed and complied with by the mainstream POSs. Rigorous formalization of ARINC 653 can reveal hidden errors in this standard and provide a necessary foundation for formal verification of POSs and ARINC 653 applications. For the purpose of reusability and efficiency, a novel methodology by integrating ontology and refinement is proposed to formally specify and analyze POSs in this paper. An ontology of POSs is developed as an intermediate model between informal descriptions of ARINC 653 and the formal specification in Event-B. A semiautomatic translation from the ontology and ARINC 653 into Event-B is implemented, which leads to a complete Event-B specification for ARINC 653 compliant POSs. During the formal analysis, six hidden errors in ARINC 653 have been discovered and fixed in the Event-B specification. We also validate the existence of these errors in two open-source POSs, i.e., XtratuM and POK. By introducing the ontology, the degree of automatic verification of the Event-B specification reaches a higher level.

In order to facilitate proof of correctness, micro-kernels are based on simplicity, providing an application only with the minimal set of features it needs in order to to work. However, simplicity alone does not guarantee the absence of bugs and software errors, and the complexity of an OS often makes such problems difficult to find and fix. In this work, we prove the functional correctness of an abstract model for the C implementation of the cyclic linked list in the real-time micro-kernel FreeRTOS, which is used in the FreeRTOS scheduler, its correctness being of critical importance for the real-time properties of FreeRTOS. The formal specification of the functional properties of FreeRTOS also provides a guide for a correct use of the functions that the implementation provides, since it lacks checks on the data. Additionally, we prove the correctness of the machine code resulting from compiling the implementation targeting the ARM architecture. Following a verification approach based on refinement, we first construct the abstract model of the implementation, where we prove both the cyclic linked list invariant and the correctness of the implementation behaviour for any list in the heap using separation logic. Second, we leverage existing machine code verification frameworks to get a HOL model of the FreeRTOS linked list compiled machine code, and we apply forward simulation to prove that such a machine code model refines the abstract model, and therefore satisfies the properties already proven over the specification.

Standards play the key role in safety-critical systems. Errors in standards could mislead system developer's understanding and introduce bugs into system implementations. In this paper, we present an Event-B formalization and verification for the ARINC 653 standard, which provides a standardized interface between safety-critical real-time operating systems and application software, as well as a set of functionalities aimed to improve the safety and certification process of such safety-critical systems. The formalization is a complete model of ARINC 653, and provides a necessary foundation for the formal development and verification of ARINC 653 compliant operating systems and applications. Three hidden errors and three cases of incomplete specification were discovered from the verification using the Event-B formal reasoning approach.

In Service-Oriented Architecture (SOA), web services container demands to support QoS (Quality of Service) hierarchical control to provide the optimization of utilization for web services container as well as a guarantee of the QoS requirements of the services. With the spreading of SOA and the improvement of research in web service, the optimization for web services container is changing from solely seeking high performance to balancing utilization on multiple levels. Therefore, web services container needs to support QoS hierarchical control based on different measurements of utilization. In order to support QoS hierarchical control with multiple measurements of utilization, a representation method of web service QoS hierarchical control is proposed, which represents different QoS hierarchical control strategies with different measurements for utilization by a single standard. Based on the representation method, we present a QoS hierarchical control mixed strategy, which can support QoS hierarchical control with multiple measurements for utilization. Using the QoS hierarchical control mixed strategy, we realize a web services container. The result of the test shows that the web services container realized can support QoS hierarchical control with different measurements for utilization. The utilization of the service container significantly improves when the mixed strategy measures utilization from multiple perspectives, add the performance of which is slightly better than that of other QoS hierarchical control strategies that measures utilization from a single perspective.

With the rapid development of the Internet, web service technology has been extensively used in distributed applications and is highly likely to replace other various technologies for the distributed application development. However, concerning most hard issues of the web services authentication, no proper solutions have been discovered and available for use now. Due to its dynamic and cross-domain characteristics, web services authentication is confronted with new challenges and difficulties. Each service or autonomous domain may have their separate authentication technologies and identity token types. Meanwhile, the same services may adopt different authentication technologies in terms of different application scenarios. Therefore, the difficult question arises as how to design an integrated and flexible architecture to enhance trust in web services. According to our findings, presented in this paper is a policy-based architecture for web services authentication termed PBA4WSA. Compared with the other architectures, the PBA4WSA can better satisfy the characteristics of web services.

Modern avionics architecture is evolving from traditional federated architecture to Integrated Modular Avionics (IMA) architecture. ARINC653 standard, which is employed in the avionics industry, supports partitioning core concept in IMA. Furthermore, avionic software has very high safety and reliability requirements in safety- critical domains. Therefore, how to develop high-integrity avionics software constructed on ARINC653 architecture becomes a very significant problem nowadays. In this paper we propose an automatic RT-Java code generation approach based on the AADL model for ARINC653 (AADL653) to enable the development of RT-Java ARINC653-based avionics software more productive and trustworthy. Our main contribution in this paper includes: (1) a mapping from the AADL653 model to a high-integrity RT-Java programming model for ARINC653 (RT-Java653); (2) an ARINC653-compliant RT-Java code generation algorithm suitable for complex multi-task collaboration interaction situation. Accordingly, we implement this RT-Java class library and corresponding code generator. Moreover, a simplified multi-task flight application as a case study is given to illustrate our approach and the preliminary experiment results show the validity of our approach.

Service Oriented Architecture (SOA) is a new form of distributed software architecture, which promotes loose-coupling and coarse-granularity. It deploys, composes and calls application components in a distributed way on Internet. The dynamics of Internet environment poses challenge to dynamic service oriented system. The distributive Internet environment requires SOA to be more distributive and self-adaptive, and choreography emphasizes the collaboration between services. Also, more flexible and dynamic software architecture is demanded for service-based software. A strong constraint mechanism which describes architectural limitation of run-time system is needed to make sure the system runs correctly. The main contribution of this paper is a graph grammar based modeling and verification approach for constrained evolution of service-oriented system. System specification described by SOA pattern and structural constraints and their satisfaction checking algorithms are proposed. We have implemented a constrained evolution verification tool that allow us to model runtime SOA, constraints and verify consistency at design-time. Further, a constraint decomposition method towards member services is given for the non-central executable SOA. And we described an adaptive collaboration policy between services to verify consistency when evolution occurs at runtime. A runtime environment's architecture for constraint evolution service oriented system is also proposed.

The widely used geospatial web services technology has provided a new means for geospatial data interoperability. Web Map Service (WMS) is a standardized geospatial web service from the Open Geospatial Consortium (OGC). WMSs can be used for requesting and producing maps on the Internet, and have been widely adopted in the Geographic Information System (GIS) community. These WMSs make remote sensing data available to a wider range of public users than ever before. However, the performance of current OGC-Compatible WMS servers can not satisfy the need of massive remote sensing data visualization. To implement a performance-optimized WMS server, we propose a global remote sensing data hierarchical model based on tile imagery pyramid and quad tree techniques for data organization and index, and adopt Hilbert curve allocation method (HCAM) for data placement. On this basis, we implement an OGC compatible tiled WMS and a service wrapper for mapping WMS to Web Services. Finally, we evaluate the tiled WMS server using real remote sensing datasets. Experiment results demonstrate a high-performance data access.

Increasingly, software needs to dynamically adapt its structure and behavior at runtime in response to changing conditions in the supporting computing, network infrastructure, and in the surrounding physical environments. By high complexity, assurance of high dependability of these software is a great challenge. Effective modeling of behavior and flexibly specifying requirements are the key issues for developing trusted adaptive software. This paper introduces a formal model for the behavior of adaptive software and an extended linear temporal logic to specify global properties. We use state machines to describe programs in different behavioral modes of adaptive software and consider these machines as different versions of programs. Specifications are classified into three categories, local, adaptation and global properties from perspective of dynamic adaptation. To specify and verify global properties on our model, we propose the versioned LTL (vLTL) which extends Linear Temporal Logic by adding version related element and enables describing properties on different versions. We also discuss verifying approach of vLTL by transforming them into LTL formulae and illustrate a study case.

Web service runtime is an important infrastructure middleware for service-based applications. It processes exchanged messages according to web service protocols. Correct implementation of web service protocols is critical for ensuring the reliability of web service runtime. In this paper, we first introduce a Service-Oriented Description Language (SODL) to precisely and concisely describe message processing logics for web service protocol implementations. Then, we propose a formal model for verifiable web service runtime, named FSM4WSR, based on Estelle (an ISO formal description standard). FSM4WSR uses module and channel to capture the essential components of the runtime architecture. Furthermore, the internal behaviors in each module are formally described by using a combination of the extended finite-state machine and SODL. Based on FSM4WSR, we automatically generate the web service protocol implementations and construct a verifiable web service runtime system, named XServices SODL Runtime.

Integration between business processes and business rules is necessary for some applications which not only hold numerous business knowledge or policies but also need the intercommunication among some distributed and heterogeneous components. This paper proposes a main process and multiple bypass process to focus the integration occurring between a bypass process and a rule set. In order to hold the context of some external services decided by business rules, we design a special scope activity in the bypass process. Moreover, an architecture and an algorithm are provided to illustrate the interaction between a BPEL engine and a rule engine for the integrating BPEL processes and business rules.

Avionics software is safe-critical embedded software and its architecture is evolving from traditional federated architectures to Integrated Modular Avionics (IMA) to improve resource usability. ARINC653, as a standard widely employed in the avionics industry, supports partitioning concepts in accordance with the IMA philosophy. To insure the development of the avionics software constructed on ARINC653 operating system with high reliability and efficiency, we propose a model-driven design methodology based on Architecture Analysis &Design Language (AADL) for ARINC653 system. This paper focus on the modeling parts of this methodology which main feature is separating the abstract application function logic represented by AADL Platform-Independent Model (AADL PIM) from the concrete execution architecture represented by AADL Model for ARINC653 (AADL653). Additionally, we provide a refined transformation framework with formally transformation rules to transform AADL PIM to AADL653 automatically and the transformation result model AADL653 can then be used for analysis, verification and code generation.

The implementation of Web services specifications is the key issue of Web services container which is the infrastructure of SOC. The specifications are always depicted in natural language, which may lead to misunderstanding or ambiguity. In this situation, the implementations of the same specification by different containers will re-introduce interoperability which is supposedly addressed by Web services. These may lead to the reliability problems among upper applications. Currently, formal methods is a precise mathematic way to model the specifications and verify the correctness of the properties. To solve the issues, first, we introduce an XML programming language called SODL (Service-Oriented Description Language) to describe the implementation of specifications. Then, using SODL, we describe the message processing logic according to specifications and implement a Web services container. Furthermore, the logic described in SODL can be converted to automata, by which lots of tools can be applied to verify the properties of container according to the specifications.

Web Map Service(WMS) is an Open Geospatial Consortium (OGC) data visualization service used for requesting and producing maps on the internet. OGC WMS has been widely adopted in the Geographic Information System (GIS) community. These WMSs make remote sensing data available to a wider range of public users than ever before. However, the performance of current WMS servers can not satisfy the need of massive remote sensing data visualization. To implement a performance-optimized WMS server, we propose a global remote sensing data hierarchical model based on image pyramid and tiling techniques for data organization. On this basis, we implement an OGC compatible tiled WMS service and a service wrapper for mapping WMSs to Web Services. Finally, we evaluate the tiled WMS server using real remote sensing datasets. Experiment results demonstrate a high-performance data access.

In the past few years, the Web has become a de facto deployment environment for new application systems. Web-based Geospatial image map systems make satellite remote sensing data available to a wider range of public users than ever before. The storage and organization of global massive multi-dimensional remote sensing data have a big impact on the performance of Web mapping systems. To implement a performance-optimized Web mapping system, we propose a global grid division pyramid hierarchical data model for massive remote sensing data management, and adopt Hilbert curve allocation method for data placements. Collaborative web map browsing is also very important for many applications such as crisis management, military activities and government decision-making. However, realizing collaboration functionality on the basis of the stateless HTTP protocol, optimized for client requests, is not trivial. The limitations of the Web's request/response architecture prevent server from pushing real-time dynamic Web data. To address this problem, we propose a web-based interactive collaborative browsing framework based on server push technique (Comet). Moreover, we develop a prototype system called ACTGIS. Finally, we evaluate the prototype system using real remote sensing datasets, which demonstrate the good performance data access in our system.

QoS-based service selection becomes a commonly accepted procedure to support rapid and dynamic web service composition. In this paper, we study the problem of QoS-based service selection in distributed QoS management environments where QoS values of alternative services are maintained by distributed QoS registries. A distributed heuristic approach is proposed to solve the problem efficiently with a high approximation ratio, and enable adaptability in distributed cross-organization environments with data privacy protection and a low cost of communication. The proposed approach consists of four stages in which variable elimination is used to reduce the size of the problem; constraint decomposition allows performing service selection independently on each QoS registry; supplementary service selection and concentrated optimization improve the approximation ratio. Performance analyses and simulation experiments show that the proposed approach performs efficiently with close-to-optimal results and fits well to distributed QoS management environments.

Current BPEL engine products are difficult to meet the highly concurrent demands of increasing mission-critical business processes application. We follow the ideas of SEDA and propose a new architecture for high-concurrency BPEL engine, which we call SEDA4BPEL. In SEDA4BPEL, the implementation of BPEL related web services protocols is encapsulated into four primary event-driven stages, to provide independence, isolation and modularity. We also introduce two controllers to manage excessive concurrent process instances. We present the SEDA4BPEL design and the implementation of a BEPL engine based on this architecture. The evaluation results show that SEDA4BPEL applications exhibit high performance and robustness when handling massive concurrency.

Service oriented system is very popular in both academic and industry. One reason is that a new complex application can be agilely implemented via the collaboration of the existent services. In the dynamic Web service environment, the Web service based applications often suffer from the leaving of component services dynamically, which will result in partial executed conversations, namely the inconsistency of the system. In the paper, we discuss how the inconsistency is produced and present an approach to handle the problem, preserving the system consistency.

Service Oriented Architecture (SOA) is a new form of distributed software architecture. SOA promotes loose coupling, services distribution, dynamicity and agility. Services involved in an SOA are remote and autonomous services, the SOA designer can not control them and unpredictable behavior can occur. This makes the SO different from other architectures for its special architecture elements and its dynamic and evolving structure. How to model this specific architecture and support service-oriented development is unimportant research field in service-oriented software engineering community. This paper proposed a graph transformation based approach to model SOA and its evolution at runtime. Graph grammar is used tore present the architectural style, type and structural constraints are introduced to improve the robustness and adaptability when reconfiguring the architectures at runtime.

Due to unpredictable failures in the network or the components, tree-structure, one of the common structures of distributed system, is partial fault-tolerance. A simple but effective method to enhance the reliability of a tree is to maintain a neighbor set for each node in the tree. Obviously, a larger neighbor set results in a higher reliability, but also increases the maintenance cost. The contribution of the paper is to give an algorithm to figure out the reliability of a tree theoretically. We also give an analysis of the results that obtained through the algorithm with various inputs.

Visualization and collaboration of large scale data sets on Internet is still one of biggest challenges in scientific visualization. A distributed, real-time, collaborative system for large scale data like seismic model can be a valuable tool to support scientific research. In this paper, we present a new approach for Web-based synchronized collaborative visualization of large scale data using Web services and rich Web clients which supports collaborative visualization in Web browsers. We use WS-resources in WSRF (Web services resource framework) to maintain states collaborative server. On client side, we design an Ajax-based (asynchronous JavaScript and XML) application using standard Web technologies. A collaborative demonstration of 3D seismic model which is 2GB size is presented and experimental results are showed finally.

Scientific collaboration has become more and more important in current scientific research. A collaboration environment which simplifies integration and collaboration of heterogeneous scientific resources, for instance scientific computing software and scientific apparatuses, can accelerate progress of scientific research remarkably. We present a novel middleware to facilitate development of distributed and collaborative application for scientific research. A service-oriented collaboration bus is proposed to enable scientific resources to be plugged in and users to interact with these resources collaboratively and transparently. Collaboration bus engines in different organizations can interoperate with each other to support distributed collaboration. We also show our prototype implementation of this middleware and a demonstration of Collaborative Visualization System for Seismic Data in earth science.