Verilog is a hardware description language (HDL) that has become an industry-standard HDL of IEEE. Multithreaded discrete event simulation language (MDESL) is a Verilog-like language. Previously, we have studied the operational semantics and denotational semantics for MDESL. This article investigates the soundness and completeness of the operational semantics for MDESL based on the denotational semantics. We introduce the concepts of transitional condition and phase semantics for each transition to show the relationship between a transition and variables in the denotational model. Then, we give the definition for the soundness and completeness of the operational semantics for MDESL. Based on our definition of the operational semantics of MDESL, we investigate the detailed theoretical proof for the soundness and completeness. Finally, a practical approach complements the theoretical one. We apply the proof assistant Coq to verify the soundness and completeness of the operational semantics for MDESL. Our research demonstrates the consistency between operational and denotational semantics for MDESL through theoretical and practical approaches.

Some examples of systems and their organizations that have ignored or violated human values have caused very devastating and widespread damage. To prevent these incidents, operationalizing human values in systems transforms the values into concrete concepts such that they can be validated. There are several challenges such as a lack of techniques to integrate values, mechanisms to trace values, formalized perspective of values. To address these challenges, we propose Ont4Sys, an ontology-based tool of semantic representation and verification for traceability models with human value. Our research uses the formal theory Ontology to integrate value into the model and traces value under traceability’s guidance. The verification and labeling algorithm is provided to verify values and help with inspections. Two subject systems are selected for feasibility and accuracy evaluation. The experimental results show that our approach can effectively verify human values; moreover, based on traceability, there is at least a 50% reduction rate in model size to help with inspections. The labeling algorithm ensures high recall while minimizing the "noise" that is detrimental to the user’s understanding of the system.

Android apps are ubiquitous and serve many aspects of our daily lives. Ensuring their functional correctness is crucial for their success. To date, we still lack a general and in-depth understanding of functional bugs, which hinders the development of practices and techniques to tackle functional bugs. To fill this gap, we conduct the first systematic study on 399 functional bugs from 8 popular open-source and representative Android apps to investigate the root causes, bug symptoms, test oracles, and the capabilities and limitations of existing testing techniques. This study took us substantial effort. It reveals several new interesting findings and implications which help shed light on future research on tackling functional bugs. Furthermore, findings from our study guided the design of a proof-of-concept differential testing tool, RegDroid, to automatically find functional bugs in Android apps. We applied RegDroid on 5 real-world popular apps, and successfully discovered 14 functional bugs, 10 of which were previously unknown and affected the latest released versions—all these 10 bugs have been confirmed and fixed by the app developers. Specifically, 10 out of these 14 found bugs cannot be found by existing testing techniques. We have made all the artifacts (including the dataset of 399 functional bugs and RegDroid) in our work publicly available at https://github.com/Android-Functional-bugs-study/home.

One of the major challenges confronting System Modeling Language(SysML) is that it cannot always provide verifiable guarantees of formalization and rigorousness.To verify model designs, the research of transformation from SysML to ontology emerges because of ontology's formal standards and verifiability obtained by ontology reasoners.However, existing transformation approaches are mostly limited to a single view without traceability or lack a clear process so that it can't be automated.In this paper, we propose a novel approach to maintain precious traceability between requirements and model multi-views design based on ontology.In addition, our approach contains a normative process of ontology building in support of an automated implementation.We use this approach to obtain the ontology of a safety-critical system and carry out the ontology evaluation experiment, whose results demonstrate the feasibility and efficiency of our approach.

Formal methods are promising for modeling and analyzing system requirements. However, applying formal methods to large-scale industrial projects is a remaining challenge. The industrial engineers are suffering from the lack of automated engineering methodologies to effectively conduct precise requirement models, and rigorously validate and verify (V&V) the generated models. To tackle this challenge, in this paper, we present a systematic engineering approach, named Formal Requirement Engineering Platform in Aircraft (FREPA), for formal requirement modeling and V&V in the aerospace and aviation control domains. FREPA is an outcome of the seamless collaboration between the academy and industry over the last eight years. The main contributions of this paper include 1) an automated and systematic engineering approach FREPA to construct requirement models, validate and verify systems in the aerospace and aviation control domain, 2) a domain-specific modeling language AASRDL to describe the formal specification, and 3) a practical FREPA-based tool AeroReq which has been used by our industry partners. We have successfully adopted FREPA to seven real aerospace gesture control and two aviation engine control systems. The experimental results show that FREPA and the corresponding tool AeroReq significantly facilitate formal modeling and V&V in the industry. Moreover, we also discuss the experiences and lessons gained from using FREPA in aerospace and aviation projects.

Abstract The hardware description language Verilog has been standardized and widely used in industry. Multithreaded Discrete Event Simulation Language (MDESL) is a Verilog-like language and it contains a rich variety of interesting features such as the event-driven computation and shared-variable concurrency as well as the realtime feature. In this paper, we present the denotational semantics for MDESL based on UTP. First a discrete time semantic model is proposed to describe the observation-oriented semantics for MDESL. The observations record the change of variables of atomic actions over time. Then the healthy formulae are defined to denote all different behaviors of programs and the semantics of programs is expressed in terms of healthy formulae. In addition, we demonstrate some interesting properties about the MDESL programs expressing as algebraic laws and their proofs are supported by our formalized denotational semantics. Our theoretical approach is complemented by a practical one, we use the theorem proof assistant Coq to formalize the UTP-based semantics for MDESL. The correctness of the algebraic laws is also verified via the mechanical approach in Coq. Our work provides a novel way to verify the correctness of UTP-based semantics forMDESL both in a theoretical approach and in a practical approach. It is also a new attempt for the application of Coq in the mechanized semantics.

Due to the existence of resource variations, it is very challenging for Cloud workflow resource allocation strategies to guarantee a reliable Quality of Service (QoS). Although dozens of resource allocation heuristics have been developed to improve the QoS of Cloud workflow, it is hard to predict their performance under variations because of the lack of accurate modeling and evaluation methods. So far, there is no comprehensive approach that can quantitatively reason the capability of resource allocation strategies or enable the tuning of parameters to optimize resource allocation solutions under variations. To address the above problems, this paper proposes a novel framework that can evaluate and optimize resource allocation strategies effectively and quantitatively. By using the statistical model checker UPPAAL-SMC and supervised learning approaches, our framework can: i) conduct complex QoS queries on resource allocation instances considering resource variations; ii) make quantitative and qualitative comparisons among resource allocation strategies; iii) enable the tuning of parameters to improve the overall QoS; and iv) support the quick optimization of overall workflow QoS under customer requirements and resource variations. The experimental results demonstrate that our automated framework can support both the Service Level Agreement (SLA) negotiation and workflow resource allocation optimization efficiently.

Although there has been substantial research in system analytics for risk assessment in traditional methods, little work has been done for safety risk prediction in communication-based train control (CBTC) system, especially intelligently predicting risk caused by the uncertainty in the system operation. Risk prediction and assessment of hazards in train control systems are vital for the safety and efficiency of urban rail transit. In this paper, we propose an intelligent hazard-risk prediction model based on a deep recurrent neural network for a new communication-mode CBTC system. First, a train-to-train communication-based train control (T2T-CBTC) system is proposed to improve the drawback of CBTC in information-exchanging mode. Then we design a risk prediction feature selection and generation method and estimate a critical function feature in the T2T-CBTC system by statistical model checking. Finally, we construct our intelligent hazard-risk prediction model based on a deep recurrent neural network using a long-short-term memory (LSTM) network. The model had excellent risk prediction classification results and performance in our experiment, even for unbalanced data set. This model consistently outperforms the deep belief network trained in Accuracy, Precision, Recall and F1-score for the hazard-risk prediction problem. Specifically, the mean accuracy is 97.2% and mean F1-score is 93.9% in overall performance of model. The improvements of our model against DBN model are 8.2% for Precision, 7% for Recall and 8% for F1-score.

There is a pressing need to verify robustness of classification deep neural networks (CDNNs) as they are embedded in many safety-critical applications. Existing robustness verification approaches rely on computing the over-approximation of the output set, and can hardly scale up to practical CDNNs, as the result of error accumulation accompanied with approximation. In this paper, we develop a novel method for robustness verification of CDNNs with sigmoid activation functions. It converts the robustness verification problem into an equivalent problem of inspecting the most suspected point in the input region which constitutes a nonlinear optimization problem. To make it amenable, by relaxing the nonlinear constraints into the linear inclusions, it is further refined as a linear programming problem. We conduct comparison experiments on a few CDNNs trained for classifying images in some state-of-the-art benchmarks, showing our advantages of precision and scalability that enable effective verification of practical CDNNs.

Verilog is a hardware description language (HDL) that has been standardized and widely used in industry. Multithreaded discrete event simulation language (MDESL) is a Verilog-like language. It contains interesting features such as event-driven computation and shared-variable concurrency. This article considers how the algebraic semantics links with the operational semantics for MDESL. Our approach is from both the theoretical and practical aspects. The link is proceeded by deriving the operational semantics from the algebraic semantics. First, we present the algebraic semantics for MDESL. We introduce the concept of head normal form. Second, we present the strategy of deriving operational semantics from algebraic semantics. We also investigate the soundness and completeness of the derived operational semantics with respect to the derivation strategy. Our theoretical approach is complemented by a practical one, and we use the theorem proof assistant Coq to formalize the algebraic laws and the derived operational semantics. Meanwhile, the soundness and completeness of the derived operational semantics is also verified via the mechanical approach in Coq. Our approach is a novel way to formalize and verify the correctness and equivalence of different semantics for MDESL in both a theoretical approach and a practical approach.

In automobile industry, it is a common approach to develop automobile real-time operating systems under some standards. For instance, OSEK/VDX is a world-wide adopted open standard. Traditional workflow is to first understand the standard, design and develop a system, then test its conformance to the standard, and finally deploy. There are several issues with the traditional workflow, e.g., ambiguities in standards may lead to incorrect design and implementation of real-world systems; the conformance of real-world systems to standards is difficult to check; and bug fixing after implementation is costly. To remedy the situation, in this paper, we present a unified executable formal automobile kernel under OSEK/VDX standard by defining the operational semantics of the system services in the standard using a rewrite-based executable semantic framework called$\mathbb {K}$. The formal kernel isunifiedin that it serves multiple purposes such as: 1) formal modeling of the OSEK/VDX standard helps detect ambiguities in the standard; 2) the executable kernel is essentially a formal model of the standard, which can be used to verify the correctness of automobile applications; and 3) verified applications can be used as test cases to check the conformance of a real-world automobile operating system against the OSEK/VDX standard. Using the formal kernel, we identify several ambiguities in the OSEK/VDX standard and a potential deadlock vulnerability in an industrial automobile application.

Abstract We propose a novel algorithm for the satisfiability problem for linear temporal logic (LTL). Existing automata-based approaches first transform the LTL formula into a Büchi automaton and then perform an emptiness checking of the resulting automaton. Instead, our approach works on-the-fly by inspecting the formula directly, thus enabling to find a satisfying model quickly without constructing the full automaton. This makes our algorithm particularly fast for satisfiable formulas. We construct experiments on different pattern formulas, the experimental results show that our approach is superior to other solvers under automata-based framework.

Satisfiability checking for Linear Temporal Logic (LTL) is a fundamental step in checking for possible errors in LTL assertions. Extant LTL satisfiability checkers use a variety of different search procedures. In this paper, we propose an LTL satisfiability-checking framework that is accelerated by leveraging the state-of-the-art Boolean SAT techniques. Our approach is based on the variant of the obligation-set method, which we proposed in earlier work. We describe here heuristics that allow the use of a Boolean SAT solver to analyse the obligations for a given LTL formula. Moreover, we show the heuristics can be also utilized as the preprocessor for every LTL satisfiability solver. The experimental evaluation indicates that the new approach provides a significant performance improvement compared to its previous version, and becomes competitive with other state-of-the-art solvers.

Formal methods advocate the crucial role played by the algebra of programs in specification and implementation of programs. Study leads to the conclusion that both the top-down approach (with denotational model as its origin) and the bottom-up approach (a journey started from operational model) can meet in the middle with a program algebra. This paper proposes a new approach on linking theories of programming. Given a program algebra, we construct a test operator taking a test case and the testing program as its arguments. The operator yields a collection of observations of the test outcomes. The denotational model of a program can be derived as a binary relation which relates the test cases with their outcomes. An operational model is considered as consistent if its step relation is consistent with the algebraic semantics.

Interrupts play an important role in real time and embedded systems. It is purposely designed to handle unexpected and emergent issues. However, the randomicity of interrupts brings some potential safety problems, i.e., too frequently interrupt handling would cause the interrupted program to miss its deadline. It is therefore difficult to precisely predict and formally reason about a program's behavior in the presence of interrupts. In this paper, we move one step forward by proposing a probabilistic denotational model for an interrupt modeling language that is capable of describing programs with nested interrupts, to characterise the formal semantics of such programs from a quantitative perspective under Hoare and He's UTP framework. On top of the denotational model, we also present a set of algebraic laws involving distinct features. Our model sets up a semantic foundation for the analysis and reasoning about programs with nested interrupts for embedded systems.

Data flow testing (DFT) focuses on the flow of data through a program. Despite its higher fault-detection ability over other structural testing techniques, practical DFT remains a significant challenge. This paper tackles this challenge by introducing a hybrid DFT framework: (1) The core of our framework is based on dynamic symbolic execution (DSE), enhanced with a novel guided path search to improve testing performance, and (2) we systematically cast the DFT problem as reach ability checking in software model checking to complement our DSE-based approach, yielding a practical hybrid DFT technique that combines the two approaches' respective strengths. Evaluated on both open source and industrial programs, our DSE-based approach improves DFT performance by 60~80% in terms of testing time compared with state-of-the-art search strategies, while our combined technique further reduces 40% testing time and improves data-flow coverage by 20% by eliminating infeasible test objectives. This combined approach also enables the cross-checking of each component for reliable and robust testing results.

Abstract As a system-level modelling language, SystemC possesses several novel features such as delayed notifications, notification cancelling, notification overriding and delta-cycle. It also has real-time and shared-variable features. Previously we have studied an operational semantics for SystemC Peng et al. (An operational semantics of an event-driven system-level simulator, pp 190–200, 2006 ) and bisimulation has been introduced based on some aspects of reasonable abstractions. The denotational method is another approach to studying the semantics of a programming language. It provides the mathematical meaning to programs and can predict the behaviour of programs. Due to the novel features of SystemC, it is challenging to study the denotational semantics for SystemC. In this paper, we applyUnifying Theories of Programming(abbreviated asUTP) Hoare and He (Unifying theories of programming, 1998 ) in exploring the denotational semantics. Two trace variables are introduced, one to record the state behaviours and another to record the event behaviours. The timed model is formalized in a threedimensional structure. A set of algebraic laws is explored, which can be proved via the presented denotational semantics. In this paper, we also consider the linking between denotational semantics and algebraic semantics. The linking is obtained by deriving the denotational semantics from algebraic semantics for SystemC. A complete set of parallel expansion laws is explored, where the location status of an instantaneous action is studied. The location status indicates an instantaneous action is due to which exact parallel component. We introduce the concept of head normal form for each program and every program is expressed in the form of guarded choice with location status. Based on this, the derivation strategy for deriving denotational semantics from algebraic semantics is provided.

We consider here Linear Temporal Logic (LTL) formulas interpreted over finite traces. We denote this logic by LTLf. The existing approach for LTLfsatisfiability checking is based on a reduction to standard LTL satisfiability checking. We describe here a novel direct approach to LTLfsatisfiability checking, where we take advantage of the difference in the semantics between LTL and LTLf. While LTL satisfiability checking requires finding a fair cycle in an appropriate transition system, here we need to search only for a finite trace. This enables us to introduce specialized heuristics, where we also exploit recent progress in Boolean SAT solving. We have implemented our approach in a prototype tool and experiments show that our approach outperforms existing approaches.

Linear Temporal Logic (LTL) is been widely used nowadays in verification and AI. Checking satisfiability of LTL formulas is a fundamental step in removing possible errors in LTL assertions. We present in this paper Aalta, a new LTL satisfiability checker, which supports satisfiability checking for LTL over both infinite and finite traces. Aalta leverages the power of modern SAT solvers. We have conducted a comprehensive comparison between Aalta and other LTL satisfiability checkers, and the experimental results show that Aalta is very competitive. The tool is available at www.lab205.org/aalta.

Summary form only given. Hybrid systems are composed by continuous physical component and discrete control component where the system state evolves over time according to interacting law of discrete and continuous dynamics. Combinations of computation and control can lead to very complicated system designs We treat more explicit hybrid models by providing a hybrid relation calculus, where both clock and signal are introduced to coordinate activities of various components of hybrid systems. This paper presents a hybrid parallel programming language with a set of novel combinators to model physical world and its interaction with the control program. We discuss the algebraic properties of the language, and show how to convert a hybrid automata to a hybrid program. The paper also demonstrates how to transform a hybrid program into a normal form using the algebraic laws of the language, and explores the link between the hybrid relation calculus and the classical relation calculus.

We propose a novel algorithm for the satisfiability problem for Linear Temporal Logic (LTL). Existing approaches first transform the LTL formula into a B"uchi automaton and then perform an emptiness checking of the resulting automaton. Instead, our approach works on-the-fly by inspecting the formula directly, thus enabling finding a satisfying model quickly without constructing the full automaton. This makes our algorithm particularly fast for satisfiable formulas. We report on a prototype implementation, showing that our approach significantly outperforms state-of-the-art tools.

The specification of Modeling and Analysis of Real-time and Embedded Systems (MARTE) is an extension of UML in the domain of real-time and embedded Systems. However, unified modeling of continuous and discrete variables in MARTE is still an unsolved problem for hybrid real-time system development. In this paper we propose an extended statechart, Hybrid MARTE statechart, for modeling and analyzing of hybrid real-time and embedded systems. In Hybrid MARTE Statecharts, we unify the logical time and the chronometric time variables. The improvement of MARTE statechart is based on hybrid automata. Formal syntax and semantics of Hybrid MARTE statecharts are given based on labeled transition systems. At the end of this paper, a case study is given to show how to model the behavior of a Train Control System with Hybrid MARTE statecharts.

Interrupt behaviors are extremely difficult to verify and reason about in the development of operating system due to their randomicity and nondeterminism. This paper proposes a formal model of interrupt program which is an extension of Dijkstra's language of guarded commands. The probabilistic operational semantics exhibiting how the effect of interrupt is produced is explored for the interrupt program. A number of algebraic laws for the computation properties that underlie the language are established in terms of the suggested probabilistic operational semantics. Furthermore, the time constraint of the interrupt program is elaborately specified and the corresponding verification can be carried out in our framework.

Abstract Following the trend to combine techniques to cover several facets of the development of modern systems, an integration of Z and CSP, calledCircus, has been proposed as a refinement language; its relational model, based on the unifying theories of programming (UTP), justifies refinement in the context of both Z and CSP. In this paper, we introduceCircus Time, a timed extension ofCircus, and present a new UTP time theory, which we use to give semantics toCircus Timeand to validate some of its laws. In addition, we provide a framework for validation of timed programs based on FDR, the CSP model-checker. In this technique, a syntactic transformation strategy is used to split a timed program into two parallel components: an untimed program that uses timer events, and a collection of timers. We show that, with the timer events, it is possible to reason about time properties in the untimed language, and so, using FDR. Soundness is established using a Galois connection between the untimed UTP theory ofCircus(and CSP) and our time theory.

Complex software systems typically involve features like time, concurrency and probability, where probabilistic computations play an increasing role. It is challenging to formalize languages comprising all these features. We have integrated probability, time and concurrency in one single model (called PTSC), where the concurrency feature is modelled using shared-variable based communication. Meanwhile, we have also explored the link between the operational semantics and algebraic semantics, where our approach was started from algebraic laws via head normal form. This paper considers the animation of the link between operational semantics and algebraic semantics for PTSC. Our approach is by using Prolog as the development language. Firstly we explore the animation of the operational semantics for PTSC. The link of the two semantics is proceeded via the concept of head normal form. Secondly the generation of head normal form is explored, especially the animation of parallel expansion laws. Finally we consider the animation of deriving operational semantics by a provided derivation strategy via head normal form. The results animated from the first and the third exploration indicate that our operational semantics is sound and complete with respect to head normal form (or algebraic laws in general).

Abstract This paper presents a theory of testing that integrates into Hoare and He’s Unifying Theory of Programming (UTP). We give test cases a denotational semantics by viewing them as specification predicates. This reformulation of test cases allows for relating test cases via refinement to specifications and programs. Having such a refinement order that integrates test cases, we develop a testing theory for fault-based testing. Fault-based testing uses test data designed to demonstrate the absence of a set of pre-specified faults. A well-known fault-based technique is mutation testing. In mutation testing, first, faults are injected into a program by altering (mutating) its source code. Then, test cases that can detect these errors are designed. The assumption is that other faults will be caught, too. In this paper, we apply the mutation technique to both, specifications and programs. Using our theory of testing, two new test case generation laws for detecting injected (anticipated) faults are presented: one is based on the semantic level of UTP design predicates, the other on the algebraic properties of a small programming language.

Summary form only given. This paper presents a refinement calculus for service components. We model the behaviour of individual service by a guarded design, which enables one to separate the responsibility of clients from the commitment made by the system, and to identify a component by a set of failures and divergences. Protocols are introduced to coordinate the interactions between a component with the external environment. We adopt the notion of process refinement to formalize the substitutivity of components, and provide a complete proof method based on the notion of simulations.

rCOS, the abbreviation of Refinement Calculus for Object Systems, is designed to present mathematical characterization of essential object-oriented concepts for an object-based language with a rich variety of features including subtypes, inheritance, type casting, dynamic binding and polymorphism. This paper represents an operational semantics for the rCOS language based on labeled transition systems. The result semantics shows the process of how the effects of an rCOS program are produced. It can be a secure guide for the implementation of the rCOS language, which is being carried out by our group. For the purpose of extending verifiability and functionality, a set of auxiliary language features is introduced to the rCOS language. Concurrent execution structure is designed to specify multi-threaded programs. Also the simulation is introduced to specify the observable behaviors of objects, and it can be regarded as the refinement relation defined in denotational domain to some extent.

This talk presents a theory of testing that integrates into Hoare and He’s Unifying Theory of Programming (UTP). We give test cases a denotational semantics by viewing them as specification predicates. This reformulation of test cases allows for relating test cases via refinement to specifications and programs. Having such a refinement order that integrates test cases, we develop a testing theory for fault-based testing. Fault-based testing uses test data designed to demonstrate the absence of a set of pre-specified faults. A well-known fault-based technique is mutation testing. In mutation testing, first, faults are injected into a program by altering (mutating) its source code. Then, test cases that can detect these errors are designed. The assumption is that other faults will be caught, too. We apply the mutation technique to both specifications and programs. Using our theory of testing, two new test case generation laws for detecting injected (anticipated) faults are presented: one is based on the semantic level of design specifications, the other on the algebraic properties of a programming language.

This paper presents an approach to validation and verification of the WSCDL specification. In order to validate whether the CDL document is well defined or not, we introduce OCL to precisely describe the constraints which was expressed by natural language, and design a simple validator to check the static properties of the CDL document. The validator is created based on a Java model and the Java model is generated according to the UML diagrams with OCL constraints which is used to describe CDL specification. To verify the dynamic properties of CDL document, we model the behavior of CDL document with Java, so that Java Pathfinder model checker can be applied to check the desired properties. The assert activity is introduced to the CDL specification for describing the logic properties, to facilitate the verification process. A case study is given and it shows that our approach is both effective and practical. Moreover, this approach can check almost every kinds of CDL document, even the documents including exception block or finalize block.

Different from traditional transactions, a compensable transaction relies on compensations to amend partial execution whenever an error occurs. The compensation is preserved on successful completion of its forward transaction for possibly later use. In this paper, we pay attention to the compositional structure of compensable transactions. Except for sequential and parallel compositions, other useful compositional constructs, such as speculative choice, exception handling, alternative forwarding and programmable compensation, are also investigated. All these constructs are not only devised to describe distinct business flow but also used to enhance the capability for dealing with errors, t-calculus is such a transactional language that involves a variety of primitives for composing compensable transactions in a wise way. We present a clear operational semantics for this language and the corresponding concept of bisimulation is defined, which is used to derive equational laws for compensable transactions.

Web services have become more and more important in these years, and BPEL4WS (BPEL) is a de facto standard for the Web service composition and orchestration. It contains several distinct features, including the scope-based compensation and fault handling mechanism. We have considered the operational semantics and denotational semantics for BPEL, where a set of algebraic laws can be achieved via these two models respectively. In this paper, we consider the inverse work, deriving the operational semantics and denotational semantics from algebraic semantics for BPEL. In our model, we introduce four types of typical programs, by which every program can be expressed as the summation of these four types. Based on the algebraic semantics, the strategy for deriving the operational semantics is provided and a transition system is derived by strict proof. This can be considered as the soundness exploration for the operational semantics based on the algebraic semantics. Further, the equivalence between the derivation strategy and the derived transition system is explored, which can be considered as the completeness of the operational semantics. Finally, the derivation of the denotational semantics from algebraic semantics is explored, which can support to reason about more program properties easily.

The Web Services Choreography Description Language (WS-CDL) is a newly developed specification for Web services composition to describe the observable behavior across multiple participants from a global perspective. However, this specification does not provide a formal semantics, whose informal description can lead to ambiguous understanding and different implementations. Hence, it causes difficulties for the engineering community to analyze the business behavior and ensure the correctness. In this paper, we present the semantics of WS-CDL in terms of process algebra CSP which has great advantages in designing and verifying concurrent processes. Therefore, all the properties we want to check within a WS-CDL document can be verified automatically in the CSP framework correspondingly. In addition, the exception and compensation handling mechanism, an important concept of long running transactions, is demonstrated clearly through our formalization work.

Nowadays the B/S (browser/server) architecture has become one of the most popular approaches to implement the Web service. Because of the instability of the Web environment, keeping the consistency of the data is of essential importance. Consequently we turn to formal methods intending to avoid inconsistencies in the B/S architecture. This paper describes a service-oriented system with the B/S architecture using the CSP (communicating sequential processes) method. We define the processes in the system and the behaviors of them. After the definition, we analyze the causes of inconsistencies and demonstrate that the formal definition and mechanism we made can implement an inconsistency free system, which means the inconsistency can be avoided or fixed.

In the paper, we proposed a language called BPEL0 with its formal semantics as the foundations of WSBPEL. In this paper, we follow the way Van der Aalst proposed on pattern analysis in workflow languages (2003), and present the patterns for BPEL0. Moreover, the expressiveness of BPEL0 is also embodied by means of putting these patterns in the program environment composed of other programming operators. Those properties about the patterns with its environment are captured by the algebraic laws, which can be proven in the framework of BPEL0 semantic domain.

As a system-level modelling language, SystemC possesses some new and interesting features such as delayed notifications, notification cancelling, notification overriding and delta-cycle. It is challenging to formalise SystemC. In this paper, we first select a kernel subset of SystemC and study its operational semantics. Based on the operational semantics we define a bisimulation relation, from which program equivalence is explored. Finally, we present a set of algebraic laws for the subset language, which can be proved based on the operational semantics model via bisimulation

Complex software systems typically involve features like time, concurrency and probability, where probabilistic computations play an increasing role. It is challenging to formalize languages comprising all these features. In this paper, we integrate probability, time and concurrency in one single model, where the concurrency feature is modelled using shared-variable based communication. The probability feature is represented by a probabilistic nondeterministic choice, probabilistic guarded choice and a probabilistic version of parallel composition. We formalize an operational semantics for such an integration. Based on this model we define a bisimulation relation, from which an observational equivalence between probabilistic programs is investigated and a collection of algebraic laws are explored. We also implement a prototype of the operational semantics to animate the execution of probabilistic programs

This paper discusses how to check consistency of UML requirements model which consists of a use case model and a conceptual class model with system constraints. Based on a given semantics, the requirements consistency can be defined and checked formally. The consistency among use cases and constraints are classified into five types. A system operation of interaction between actor and system is formally defined as a pair of pre and post conditions. An atomic use case is described as one system operation, and a composed use case may be defined as several system operations described by an activity diagram. Thus, each use case can also be modelled as a pair of pre and post conditions by composing the pre and post conditions of system operations by introducing a sequence composition operation. Requirement consistency can be logically checked based on the semantics. A simple library system is used as a case study to illustrate the feasibility of the method.

Conventional theories of concurrency reduce parallel processes to sequential ones. Here, we propose a true concurrency trace model which takes variables of parallel processes as a whole and runs parallel processes as simultaneous updates on variables. By equipping each resource an ownership variable, the model has a uniform treatment to both variable access conflicts and resource conflicts. A denotational semantics based on the model is studied. After that, we show how to use this model to build a correct resource scheduler, and specify pre-compilers such that the resulting systems do not incur conflicts and have less chance of deadlocks.

Abstract Computer aided hardware/software partitioning is one of the key challenges in hardware/software co-design. This paper describes a new approach to hardware/software partitioning for a synchronous communication model including multiple hardware devices. We transform the partitioning into a reachability problem of timed automata. By means of an optimal reachability algorithm, the optimal solution can be obtained with limited resources in hardware. To relax the initial condition of the partitioning for optimization, two algorithms are designed to explore the dependency relations among processes in the sequential specification. Moreover, we propose a scheduling algorithm to improve the synchronous communication efficiency further after partitioning stage. Some experiments are conducted with the model checker UPPAAL to show our approach is both effective and efficient.

Abstract. We introduce a comparative case study on the application of formal methods and techniques to the Tree Identify Protocol of the IEEE standard 1394 serial multimedia bus. The Tree Identify Protocol makes an ideal subject for this purpose because it is small yet complex, and may be modelled in a variety of ways. We provide an informal explanation of the protocol, describe how the case study was conducted, and give an overview of the results.

Hybrid systems are interactive systems of continuous devices and digital control programs. Typical examples are digital modules that control a physical environment evolving over time. The principal problem of the subject is to model them so that given a specification for the continuous component of the system, we can extract, if this is possible, from the description of the total system and the specification of the continuous component, the specification of the control program which will force the continuous device to meet its specification. This paper presents a formal description language for hybrid systems, which is an integration of CSP, which describes digital control programs, and DC for specification of continuous devices. We define primitive operators over systems in DC and prove that so defined operators meet basic algebraic laws of these operators.

Hardware and software co-design is a design technique which delivers computer systems comprising hardware and software components. A critical phase of the codesign process is to decompose a program into hardware and software.. This paper proposes an algebraic partitioning method whose correctness is verified in the algebra of programs. We introduce the program analysis phase before program partitioning and develop a collection of syntax-based splitting rules, where the former provides information for moving operations from software to hardware and reducing the interaction between components, and the latter supports a compositional approach to program partitioning.

The actual behaviour of a hardware device available for an implementation of a control system can be simulated by a program, allowing the hardware device to be proved correct by standard software techniques. In this paper we formalise event semantics of hardware description language in the form of relations and use relation calculus to prove properties (including termination, stability, and uniqueness of final state) of combinational programs, the cycle behaviour of which is defined as a conditional loop of non-deterministic choices between generalised parallel assignments.

This paper presents the derivation of an operational semantics from a denotational semantics for a subset of the widely used hardware description language Verilog. Our aim is to build equivalence between the operational and denotational semantics. We propose a discrete denotational semantic model for Verilog. A phase semantics is provided for each type of transition in order to derive the operational semantics.

We have recently proposed a formalization of the use of UML in requirement analysis. This paper applies that formalization to a library system as a case study. We intend to show how the approach supports a use case-driven, step-wised and incremental development in building models for requirement analysis. The actual process of building the models shows the importance and feasibility of the formalization itself.

A theory of programming starts with a complete Boolean algebra of specifications, and defines healthiness conditions which exclude infeasibility of implementation. These are expressed as algebraic laws useful for transformation and optimisation of designs. Programming notations and languages must be restricted to those preserving all the healthiness conditions. We have explored a wide range of programming paradigms, including nondeterministic, sequential, parallel, logical and probabilistic. In all cases, we have found a single healthiness condition, formalised by constructions due to Karoubi and to Kleisli. The uniformity maintains for all paradigms a single notion of correctness throughout the chain that leads from specification through designs to programs that are proved to meet the original specification.

An operational semantics of a significant subset of the Verilog hardware description language (HDL) is presented. The semantics is encoded using the logic programming language Prolog in a literate programming style. This allows the associated documentation to be maintained in step with the semantics, and the printed version to be presented in a standard mathematical operational semantics style. It also enables the semantics to be directly animated using a Prolog interpreter. Using this approach allows the exploration of sometimes subtle behaviours of parallel programs and the possibility of rapid changes or additions to the semantics of the language covered that could be missed otherwise. In addition, it provides and extra check on the validity of the operational semantics.

Abstract Compositional proof systems for shared variable concurrent programs can be devised by including the interference information in the specifications. The formalism falls into a category called rely-guarantee (or assumption-commitment) , in which a specification is explicitly (syntactically) split into two corresponding parts. This paper summarises existing work on the rely-guarantee method and gives a systematic presentation. A proof system for partial correctness is given first, thereafter it is demonstrated how the relevant rules can be adapted to verify deadlock freedom and convergence. Soundness and completeness, of which the completeness proof is new, are studied with respect to an operational model. We observe that the rely-guarantee method is in a sense a reformulation of the classical non-compositional Owicki & Gries method, and we discuss throughout the paper the connection between these two methods.

Abstract This paper generalizes an algebraic method for the design of a correct compiler to tackle specification and verification of an optimized compiler. The main optimization issues of concern here include the use of existing contents of registers where possible and the identification of common expressions. A register table is introduced in the compiling specification predicates to map each register to an expression whose value is held by it. We define different kinds of predicates to specify compilation of programs, expressions and Boolean tests. A set of theorems relating to these predicates, acting as a correct compiling specification, are presented and an example proof within the refinement algebra of the programming language is given. Based on these theorems, a prototype compiler in Prolog is produced.

Category theory offers a unified mathematical framework for the study of specifications and programs in a variety of styles, such as procedural, functional and concurrent. One way that these different languages may be treated uniformly is by generalising the definitions of some standard categorical concepts. In this paper we reproduce in the generalised theory analogues of some standard theorems on isomorphism, and outline their applications to programming languages.

Abstract In this paper we deal with the problem of (nondeterministic and parallel) process refinement. The basic notion of refinement is defined via the improved failure semantics of CSP [BHR84, BrR85, Hoa85, Ros88]. The concept of simulation of Communicating Systems introduced in [Mil80, Par81] is generalised and proved to be sound for the correctness of refinement. A Galois connection is presented to show that up-simulation and down-simulation together provide a complete proof method. The paper also suggests that simulation can be employed to derive an implementation from a specification.