Testing and verification of healthcare information systems is a challenging and important issue since faults in these critical systems may lead to loss of lives, and in the best cases, loss of money and reputations. However, due to the complexity of these systems, and the increasing demand for new products and new technologies in this domain, there are several methods and technologies being used for testing these systems. In this paper, we review the state of the art on testing and verification of healthcare information systems, and then we identify several open issues and challenges in the area. We divide the exiting methods into three categories: simulation based methods, formal methods, and other techniques such as semi-formal methods. Then, we discuss challenging and open issues in the domain.

Establishing the security of a system is an intricate problem with subtle nuances: it requires a careful examination of the underlying assumptions, abstractions, and possible actions. Consequently, assuring that a system behaves securely is virtually impossible without the use of rigorous analytical techniques. In this article, we focus on a single cryptographic protocol (Needham–Schroeder) and show how several different formal methods can be used to identify its various vulnerabilities. These vulnerabilities include susceptibility to freshness attacks and impersonations.

Quad trees-trees with four branches, are used to abstractly describe tree-structured carry-lookahead adders using 4-bit components. The specification and implementation descriptions are parametrized and tree-structured adders having arbitrarily large inputs and outputs are described. The descriptions are formally verified using the HOL theorem power.

Security properties such as privacy, authentication and integrity are of increasing importance to networked systems. Systems with security requirements typically must operate with a high degree of confidence, i.e. they must be highly assured. We show how the message structure of privacy enhanced mail (PEM) and the operations on PEM structures have the desired implementation independent security properties. The verification of an integrity checking function is shown in detail. Higher-order logic and the HOL theorem-prover are used to precisely relate security properties to implementation specifications.

Algorithmic state machine (ASM) descriptions or hardware flowcharts have been used successfully to describe and verify large systems like the IBM 3081. Hardware flowcharts are intuitively appealing in their specification of control flow and data path operations. Nevertheless, previous mechanizations of hardware flowcharts lacked a formal semantics which prevented a rigorous analysis of implementations refined from ASM descriptions, and the ability to equate composed ASM descriptions to purely behavioral descriptions. To address these concerns, we describe an algorithmic register transfer language which has a formal semantics along with an algebra which is used to reason about composed ASM descriptions.

Extending VLSI CAD with higher-order logic integrates formal verification with synthesis. The benefits of doing so are: 1) relating instruction-set descriptions to implementations, 2) designing at a higher level of abstraction than at the level of schematics, 3) verifying by proof 4) reusing verified parameterized designs, 5) automatically compiling designs in higher-order logic to parameterized cell generators and layouts, and 6) validating electrical and functional properties by simulation. Such an integration is demonstrated by linking the Cambridge Higher-Order Logic (HOL) theorem-prover with the Mentor Graphics GDT design environment. We illustrate its applications by creating a parameterized macro-cell generator for an n-bit Am2910 microprogram sequencer whose design is formally verified with respect to its instruction-set architecture specification.

The paper compares and contrasts various methods presently available for specification, validation and verification, with emphasis on verification. We describe an application of formal methods to protocol specification, validation, and verification, using an actual protocol as an example. We use a process algebra to build models of an OSI protocol and test these models using a model checker. Model checking allows us to verify large and complex models and use formal methods as practical solutions. We also show an example with an automated theorem prover.

System engineering requires design and verification at several levels of abstraction-from top-level process descriptions down to gate-level hardware designs. A variety of tools such as specification languages, simulators, model checkers, theorem-provers, and other computer-aided design tools are used for designing and verifying systems. These tools must be integrated to support a continuous design flow. We report on the theoretical and practical aspects of integration and discuss our experience with specific tools.

Formally verified metafunctions which synthesize array multipliers and inner product hardware of arbitrary size and structure are presented. The metafunctions operate on signed-binary inputs in general and two's-complement in particular, and are higher order. They are shown to be equivalence-preserving transformations and correctly produce multipliers and inner product hardware of arbitrary size and structure. All the metafunctions, their associated correctness theorems, and their correctness proofs are machine executable within the higher order logic (HOL) theorem prover. The function expressions produced by the metafunctions can be used as hardware synthesis descriptions or as comparison functions for Boolean-comparison-based systems. In addition to the definitions written in higher-order logic, the major definitions are written in a more informal functional programming language-like notation which should facilitate translation of the synthesis functions to other hardware description languages.>

The development of theorem-based design methods is considered. Theorem-based design uses formal logic to create provably correct implementations. Past work has focused on using formal logic and post-hoc proof for design verification. Here, the focus is on hardware synthesis functions, called hardware metafunctions, which synthesize hardware in a provably correct manner. Designs produced using the metafunctions are correct-by-construction and are formally related to their specifications by simple substitution or rewriting of terms within the correctness theorem for each metafunction. Typically, the metafunctions are parametric and, once proven correct, validate an entire class of designs. Theorem-based design is practical when the metafunctions and their proofs of correctness are machine-executable. This is accomplished using appropriate declarative languages with a strong formal basis and by developing the proofs of correctness using automatic theorem provers. The functional language SCHEME is used along with the Higher Order Logic (HOL) proof checker. An introduction to the use of higher-order logic as a design along with the verification of an adder array metafunction for an array multiplier is presented.>

Formally verified hardware synthesis functions have been developed and implemented using high-order logic, automatic theorem provers, and declarative languages. The synthesis functions, which take the form of equivalence-preserving transformations, enable implementations to be related to their specifications in a formally verified manner. As shown by the theory of design for array multipliers, verified synthesis functions produce implementations which are correct by construction, thus avoiding the exponential growth in effort inherent in simulation-based and Boolean comparison-based verification. Theories of design with their verified synthesis functions and correctness theorems represent additional features which would logically extend computer-aided design systems for design synthesis and design verification.>