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.

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.

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.

Copyright © 2017 by SCITEPRESS - Science and Technology Publications, Lda. All rights reserved. This paper sets out conditions for privacy and security of data against the privileged operator on processors that 'work encrypted'. A compliant machine code architecture plus an 'obfuscating' compiler turns out to be both necessary and sufficient to achieve that, the combination mathematically assuring the privacy of user data in arbitrary computations in an encrypted computing context.

Copyright © 2016 by SCITEPRESS - Science and Technology Publications, Lda. All rights reserved.This paper explores a new approach to encrypted microprocessing, potentiating new trade-offs in security versus performance engineering. The coprocessor prototype described runs standard machine code (32-bit OpenRISC v1.1) with encrypted data in registers, on buses, and in memory. The architecture is 'superscalar', executing multiple instructions simultaneously, and is sophisticated enough that it achieves speeds approaching that of contemporary off-the-shelf processor cores. The aim of the design is to protect user data against the operator or owner of the processor, and so- called 'Iago' attacks in general, for those paradigms that require trust in data-heavy computations in remote locations and/or overseen by untrusted operators. A single idea underlies the architecture, its performance and security properties: it is that a modified arithmetic is enough to cause all program execution to be encrypted. The privileged operator, running unencrypted with the standard arithmetic, can see and try their luck at modifying encrypted data, but has no special access to the information in it, as proven here. We test the issues, reporting performance in particular for 64-bit Rijndael and 72-bit Paillier encryptions, the latter running keylessly.

It is expected that the Internet of Things (IoT) provides the foundational infrastructure for smart cities, and making ICT an enabling technology to meet major challenges associated with climate change, energy efficiency, mobility and future services. On the other hand a smart city with these requirements is usually evolving through incremental automation and integration of new components, that are digital or physical components or smart devices. To handle the growing scale and complexity of a system, an adaptive modelling method is needed for dynamic analysis and verification and/or validation, and integration. In this paper, we consider the case study of a Demand Response (DR) Programme that is to be realized by the deployment of a network of smart meters. Through this case study, we propose a component-based modelling approach and demonstrate how it deals with the growing complex architecture.

No abstract available.

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).

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.

For aspect-oriented modular reconfigurable computing, we specify a notion of "aspect" in the context of modular reconfigurable computing systems. In our formal approach, an aspect is determined as a coalgebraic transformation on modular reconfigurable computing systems. Then, based on this fundamental concept of aspect, inheritance and super- imposition properties of aspects are studied. Specifically, the inheritance property is shown to be a bisimulation relation and the superimposition property is determined in the context of coalgebraic reconfiguration. Moreover, we also justify that our approach is sufficiently expressive to combine aspect-orientation and modular reconfigurable computing.

Fault-based testing of software checks the software implementation for a set of faults. Two previous papers on fault-based testing [Kuhn 1999; Tsuchiya and Kikuno 2002] represent the required behavior of the software as a Boolean specification represented in Disjunctive Normal Form (DNF) and then show that faults may be organized in a hierarchy. This article extends these results by identifying necessary and sufficient conditions for fault-based testing. Unlike previous solutions, the formal analysis used to derive these conditions imposes no restrictions (such as DNF) on the form of the Boolean specification.

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

Abstract This paper describes an approach to the formalization of existing criteria used in computer systems software testing and proposes a new Reinforced Condition/Decision Coverage (RC/DC) criterion. This new criterion has been developed from the well-known Modified Condition/Decision Coverage (MC/DC) criterion and is more suitable for the testing of safety-critical software where MC/DC may not provide adequate assurance. As a formal language for describing the criteria, the Z notation has been selected. Formal definitions in the Z notation for RC/DC, as well as MC/DC and other criteria, are presented. Specific examples of using these criteria for specification-based testing are considered and some features are formally proved. This characterization is helpful in the understanding of different types of testing and also the correct application of a desired testing regime.

Ten years ago, our 1995 paper Ten Commandments of Formal Methods [5] suggested some guidelines to help ensure the success of a formal methods project. It proposed ten important requirements (or "commandments") for formal developers to consider and follow, based on our knowledge of several industrial application success stories, most of which have been reported in more detail in two books [17],[18]. The paper was surprisingly popular, is still widely referenced, and used as required reading in a number of formal methods courses. However, not all have agreed with some of our commandments, feeling that they may not be valid in the long-term. We re-examine the original commandments ten years on, and consider their validity in the light of a further decade of industrial best practice and experiences.

Dynamically reconfigurable computing within embedded computer-based systems can be partially modified at runtime without stopping the operation of the whole system. In this paper, a provable algorithm for runtime evolution of a logical configuration is formally represented by the appropriate graph transformation. In other words, programming is considered as a visual transformation of the logical configuration by the formulated rules. Their soundness is proved. A logical configuration in evolution is provable from another by applying these rules. Subsequently, an algorithmic approach to programming is formally developed and analyzed

The Modified Condition Decision Coverage (MCDC) test criterion is a mandatory requirement for the testing of avionics software as per the DO-178B standard. This paper presents a formal analysis for the three different forms of MCDC. In addition, a recently proposed test criterion, Reinforced Condition Decision Coverage (RCDC), has also been investigated in comparison with MCDC. In contrast with the earlier analysis approaches that have been based on empirical and probabilistic models, the principles of Boolean ogic are used here to study the fault detection effectiveness of the MCDC and RCDC criteria. Based on the properties of Boolean specifications, the analysis identifies the detection conditions for six kinds of faults. The results allow the measurement of the effort required in testing and the effectiveness of generated test sets satisfying the MCDC and RCDC criteria. Copyright © 2004 John Wiley & Sons, Ltd.

Efficient management of the logic resource available is one of the biggest problems faced by the embedded systems based on FPGA, in which their functionality can be partially modified at run-time without stopping the operation of the whole system. When the sequence of reconfigurations to be performed is not predictable, resource allocation decisions have to be made on-line. Dynamical reconfiguration can be necessary to relocate a running physical configuration, and to rearrange the logic resources into the variety of physical portions. Our proposed algorithm is formally developed to enable implementing an on-line management of FPGA logic resources, supporting the rearrangement of running functions, releasing enough contiguous space for configuration of new incoming functions, and performing the defragmentation in a way completely transparent to the applications currently running. Therefore, on-line scheduling of tasks in the spatial and temporal domains becomes possible, enabling the implementation of virtual hardware concept.

Abstract Fault‐detection effectiveness of coverage criteria has remained one of the controversial issues in recent years. In order to detect a fault, a test set must execute the faulty statement, cause infection of the data state and then propagate the faulty data state to bring about a failure. This paper sheds some light on the earlier contradictory results by investigating the infection aspect of coverage criteria. For a given test criterion, the number of test sets satisfying the criterion may be very large, with varying fault‐detection effectiveness. In a recent work the measure of variation in effectiveness of a test criterion was defined as ‘tolerance’. This paper presents an experimental evaluation of tolerance for control‐flow test criteria by exhaustive test set generation, wherever possible. The approach used here is complementary to earlier empirical studies that adopted analysis of some test sets using random selection techniques. Four industrially used control‐flow testing criteria, Condition Coverage (CC), Decision Condition Coverage (DCC), Full Predicate Coverage (FPC) and Modified Condition Decision Coverage (MCDC) have been analysed against four types of faults. A new test criterion, Reinforced Condition Decision Coverage (RCDC), is also analysed and compared. Copyright © 2004 John Wiley & Sons, Ltd.

Effectiveness of testing criteria is the ability to detect failure in a software program. We consider not only effectiveness of some testing criterion in itself but a variance of effectiveness of different test sets satisfied the same testing criterion. We name this property "tolerance" of a testing criterion and show that, for practical using a criterion, a high tolerance is as well important as high effectiveness. The results of empirical evaluation of tolerance for different criteria, types of faults and decisions are presented. As well as quite simple and well-known control-flow criteria, we study more complicated criteria: full predicate coverage, modified condition/decision coverage and reinforced condition/decision coverage criteria.

Formal methods have traditionally been used for specification and development of software. However there are potential benefits for the testing stage as well. The panel session associated with this paper explores the usefulness or otherwise of formal methods in various contexts for improving software testing. A number of different possibilities for the use of formal methods are explored and questions raised. The contributors are all members of the UK FORTEST Network on formal methods and testing. Although the authors generally believe that formal methods are useful in aiding the testing process, this paper is intended to provoke discussion. Dissenters are encouraged to put their views to the panel or individually to the authors.

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.

Describes an approach to formalization of criteria of computer systems software testing. A brief review of control-flow criteria is introduced. As a formal language for describing the criteria, the Z notation is selected. Z schemas are presented for definitions of the following criteria: statement coverage, decision coverage, condition coverage, decision/condition coverage, full predicate coverage, modified condition/decision coverage, and multiple condition coverage. This characterization could help in the correct understanding of different types of testing and also the correct application of a desired testing regime.

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.

This paper introduces a denotational semantics for a core of the draft IEEE standard analog and mixed signal design language VHDL-AMS, and derives general results about the behaviour of VHDL-AMS programs from it. We include, for example, a demonstration that VHDL-AMS parallelism is benign in the absence of shared initializations. As proof of concept we have built an interpreted simulator that prototypes the semantics and which runs multi-process mixed analog and digital descriptions correctly.

Formal methods are used in a surprisingly wide variety of applications and ways throughout the world. While they may still be considered a niche market, there is growing evidence that they can be used successfully in industry if applied judiciously. The paper discusses same of the issues concerning the successful application of formal methods and surveys a number of examples of industrial usage, with a large bibliography for further reading on the state of the art in this area.

Abstract Top‐down (LL) context‐sensitive parsers with integrated synthesis and use of attributes are easy to express in functional programming languages, but the elegant functional programming model can also serve as an exact prototype for a more efficient implementation of the technology in ANSI C. The result is a compiler‐compiler that takes unlimited lookahead and backtracking, the extended BNF notation, and parameterized grammars with (higher‐order) meta‐parameters to the world of C programming. This article reports on the utility in question three years after public release.Preccgenerates standard ANSI C and is ‘plug compatible’ withlex‐ generated lexical analyzers prepared for the UNIXyacccompiler‐compiler. In contrast toyacc, however, the generated code is modular, which allows parts of scripts to be compiled separately and linked together incrementally. The constructed code is relatively efficient, as is demonstrated by the example Occam parser treated in depth here, but the main advantages we claim are ease of use, separation of specification and implementation concerns, and maintainability.

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.

While a compiler produces low-level object code from high-level source code, a decompiler produces high-level code from low-level code and has applications in the testing and validation of safety-critical software. The decompilation of an object code provides an independent demonstration of correctness that is hard to better for industrial purposes (an alternative is to prove the compiler correct). But, although compiler compilers are in common use in the software industry, a decompiler compiler is much more unusual. It turns out that a data type specification for a programming-language grammar can be remolded into a functional program that enumerates all of the abstract syntax trees of the grammar. This observation is the springboard for a general method for compiling decompilers from the specifications of (nonoptimizing) compilers. This paper deals with methods and theory, together with an application of the technique. The correctness of a decompiler generated from a simple occam-like compiler specification is demonstrated. The basic problem of enumerating the syntax trees of grammars, and then stopping, is shown to have no recursive solution, but methods of abstract interpretation can be used to guarantee the adequacy and completeness of our technique in practical instances, including the decompiler for the language presented here.

Abstract A compiler may be specified by a description of how each construct of the source language is translated into a sequence of object code instructions. It is possible to produce a compiler prototype almost directly from this specification in the form of a logic program. This defines a relation between allowed high‐level and low‐level program constructs. Normally a high‐level program is supplied as input to a compiler and object code is returned. Because of the declarative nature of a logic program, it is possible for the object code to be supplied and the allowed high‐level programs returned, resulting in a decompiler, provided enough information is available in the object code. This paper discusses the problems of adopting such an approach in practice. A simple compiler and decompiler are presented in full as an example in the logic programming language Prolog, together with some sample output. The possible benefits of usingconstraint logic programmingare also considered. Potential applications include reverse‐engineering in the software maintenance process, verification of safety‐critical object code, quality assessment of code and program debugging tools.

Abstract Window management systems are now used extensively for user interfaces to computer systems. In particular, X11 has come to dominate the workstation market as a widely accepted industry standard on many different hardware platforms. However, no formal standard currently exists for this window system, both in terms of an international standards body (although this is being addressed), and in terms of a precise (mathematical) specification of what the interface is intended to do. This paper advocates the use of a formal notation to describe such an important system to avoid ambiguity and undesired or unintended variations between different implementations of the same system. Theformal notation used for demonstration purposes, Z, is based on set theory, and has been developed at the Programming Research Group in Oxford.