Daniel Hoffman

dblp:h/DanielHoffman · DBLP profile ↗
← Back
28ranked-venue papers
16as first author
0since 2021 · last 2016
—ORCID · none

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 25 · 15 first-authorArtificial intelligence and machine learning · 1Systems, architecture and hardware · 1 · 1 first-authorApplied, interdisciplinary, general and emerging computing · 1

Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.

Software engineering, system software, and programming languages
9 papers
Software testing · 71% Concurrent programming · 17% Program analysis · 6%
Network and information security
1 paper
Network security · 100%

Topics — the 19 heaviest of 21, each with the papers that count most for it

TopicWeightPapersLastEvidence papers
Concurrent programming
concurrency bugs
0.122003
Tool Support for Testing Concurrent Java Components · IEEE Trans. Software Eng. 2003
A Concurrency Test Tool for Java Monitors · ASE 2001
Software testing
concurrency testing
0.122003
Tool Support for Testing Concurrent Java Components · IEEE Trans. Software Eng. 2003
A Concurrency Test Tool for Java Monitors · ASE 2001
Software testing › combinatorial testing
covering array generation
0.112005
Blowtorch: a framework for firewall test automation · ASE 2005
Software testing
test generation
0.112005
Blowtorch: a framework for firewall test automation · ASE 2005
Software testing
unit testing
0.022003
Tool Support for Testing Concurrent Java Components · IEEE Trans. Software Eng. 2003
Automated Module Testing in Prolog · IEEE Trans. Software Eng. 1991
Software testing › specification-based testing
conformance testing
0.011998
Programmatic Testing of the Standard Template Library Containers · ASE 1998
Software testing › test process › test design
test suite design
0.011998
Programmatic Testing of the Standard Template Library Containers · ASE 1998
Program analysis › static analysis
modular analysis
0.011995
State Abstraction and Modular Software Development · SIGSOFT FSE 1995
Program analysis › static analysis › abstract interpretation
state abstraction
0.011995
State Abstraction and Modular Software Development · SIGSOFT FSE 1995
Empirical software engineering
software engineering practice
0.012001
David L. Parnas Symposium · ICSE 2001
Software testing
automated testing
0.011991
Automated Module Testing in Prolog · IEEE Trans. Software Eng. 1991
Software testing › black-box testing
functional testing
0.011991
Automated Module Testing in Prolog · IEEE Trans. Software Eng. 1991
Software testing
random testing
0.011991
Automated Module Testing in Prolog · IEEE Trans. Software Eng. 1991
Software testing
test input generation
0.011991
Automated Module Testing in Prolog · IEEE Trans. Software Eng. 1991
Requirements engineering and software design › software architecture › architectural design
module interface design
0.011990
On Criteria for Module Interfaces · IEEE Trans. Software Eng. 1990
Software testing
test oracle
0.011998
Programmatic Testing of the Standard Template Library Containers · ASE 1998
Requirements engineering and software design › specification
executable specification
0.011988
Trace Specifications: Methodology and Models · IEEE Trans. Software Eng. 1988
Requirements engineering and software design › specification
software specification
0.011988
Trace Specifications: Methodology and Models · IEEE Trans. Software Eng. 1988
Internet architecture and protocols
protocol specification
0.011985
The Trace Specification of Communications Protocols · IEEE Trans. Computers 1985

Methods — techniques the papers use, named apart from their topics

traffic replay · 0.1production grammars · 0.1covering arrays · 0.1driver generation · 0.1clock synchronization · 0.1white-box testing · 0.0boundary value analysis · 0.0black-box testing · 0.0test oracle generation · 0.0prolog scripting · 0.0trace language · 0.0formal specification · 0.0
YearPublicationVenuePosition
2016 The Scale2 Multi-Network Architecture for IoT-Based Resilient Communities
abstract
Safe Community Awareness and Alerting Network (SCALE) is a community government/academic/industry partnership effort that aims to deploy, actuate and evaluate techniques to support multiple heterogeneous IoT technologies in real world communities. SCALE2, an extension of SCALE, engages a multi-tier and multi-network approach to drive data flow from IoT devices to the cloud platforms. While devices are used to gather data, most of the analytics are executed in the cloud. Managing and utilizing these multiple networks, devices and technologies is a big challenge that calls for an integrated management. In this context, we propose to leverage a related effort, MINA (Multi-network INformation Architecture), that aims at integrating operations of multi-networks IoT deployments in a hierarchical manner. This paper discusses the mapping of the SCALE2 heterogeneous platforms in the MINA environment and argues for a hierarchical approach to extending and managing community IoT multi-networks. We discuss resilience methods that can be employed at different tiers in the hierarchical architecture. We illustrate examples of how multiple applications can be supported in this heterogeneous setting; example applications include cooperative seismic event detection, mobile data collections for air quality information and assisted living for elders. Finally, we discuss novel research challenges associated with managing multi-network IoT architecture.
Md. Yusuf Sarwar Uddin, Alexander Nelson 0001, Kyle E. Benson, Guoxi Wang, Qiuxi Zhu, Nailah Saleh Alhassoun, Prakash Chakravarthi, Julien Stamatakis, Daniel Hoffman, Luke D'arcy, Nalini Venkatasubramanian
SMARTCOMP10
2014 Toward a mature industrial practice of software test automation
Hong Zhu 0002, Daniel Hoffman, John Hughes 0001, Dianxiang Xu
Softw. Qual. J.2
2011 Grammar-based test generation with YouGen
abstract
Abstract Grammars are traditionally used to recognize or parse sentences in a language, but they can also be used to generate sentences. In grammar‐based test generation (GBTG), context‐free grammars are used to generate sentences that are interpreted as test cases. A generator reads a grammar G and generates L(G), the language accepted by the grammar. Often L(G) is so large that it is not practical to execute all of the generated cases. Therefore, GBTG tools support ‘tags’: extra‐grammatical annotations which restrict the generation. Since its introduction in the early 1970s, GBTG has become well established: proven on industrial projects and widely published in academic venues. Despite the demonstrated effectiveness, the tool support is uneven; some tools target specific domains, e.g. compiler testing, while others are proprietary. The tools can be difficult to use and the precise meaning of the tags are sometimes unclear. As a result, while many testing practitioners and researchers are aware of GBTG, few have detailed knowledge or experience. We present YouGen, a new GBTG tool supporting many of the tags provided by previous tools. In addition, YouGen incorporates covering‐array tags, which support a generalized form of pairwise testing. These tags add considerable power to GBTG tools and have been available only in limited form in previous GBTG tools. We provide semantics for the YouGen tags using parse trees and a new construct, generation trees. We illustrate YouGen with both simple examples and a number of industrial case studies. Copyright © 2010 John Wiley & Sons, Ltd.
Daniel Hoffman, David Ly-Gagnon, Paul A. Strooper, Hong-Yi Wang 0012
Softw. Pract. Exp.1
2010 Two case studies in grammar-based test generation
Daniel Hoffman, Hong-Yi Wang 0012, Mitch Chang, David Ly-Gagnon, Lewis Sobotkiewicz, Paul A. Strooper
J. Syst. Softw.1
2006 Radio propagation patterns in wireless sensor networks: new experimental results
abstract
Wireless sensors use low power radio transceivers due to the stringent constraints on battery capacity. As a result, radio transmission with wireless sensors is unreliable. Further, propagation patterns are irregular, causing some links to be asymmetric. Accurate models of radio propagation patterns are important for protocol design and simulation. Thus far, measurements of radio propagation patterns have been carried out using the motes themselves for test measurement. We have carried out experiments using RF test equipment to precisely measure mote transmit and receive signal strength and to accurately determine propagation patterns. Our tests have produced new radio propagation patterns and a new propagation model. Our model is more accurate than previous models and can be used for building both analytical and simulation models for wireless sensor networks.
Tereus Scott, Kui Wu 0001, Daniel Hoffman
IWCMC3
2005 Blowtorch: a framework for firewall test automation
abstract
Firewalls play a crucial role in network security. Experience has shown that the development of firewall rule sets is complex and error prone. Rule set errors can be costly, by allowing damaging traffic in or by blocking legitimate traffic and causing essential applications to fail. Consequently, firewall testing is extremely important. Unfortunately, it is also hard and there is little tool support available.Blowtorch is a C++ framework for firewall test generation. The central construct is the packet iterator: an event-driven generator of timestamped packet streams. Blowtorch supports the development of packet iterators with a library for packet header creation and parsing, a transmit scheduler for multiplexing of multiple packet streams, and a receive monitor for demultiplexing of arriving packet streams. The framework provides iterators which generate packet streams using covering arrays, production grammars, and replay of captured TCP traffic. Blowtorch has been used to develop tests for industrial firewalls that are placed between an IT network and a process control network.
Daniel Hoffman, Kevin Yoo
ASE1
2005 Tool support for executable documentation of Java class hierarchies
abstract
While object-oriented programming offers great solutions for today's software developers, this success has created difficult problems in class documentation and testing. In Java, two tools provide assistance: Javadoc allows class interface documentation to be embedded as code comments and JUnit supports unit testing by providing assert constructs and a test framework. This paper describes JUnitDoc, an integration of Javadoc and JUnit, which provides better support for class documentation and testing. With JUnitDoc, test cases are embedded in Javadoc comments and used as both examples for documentation and test cases for quality assurance. JUnitDoc extracts the test cases for use in HTML files serving as class documentation and in JUnit drivers for class testing. To address the difficult problem of testing inheritance hierarchies, JUnitDoc provides a novel solution in the form of a parallel test hierarchy. A small controlled experiment compares the readability of JUnitDoc documentation to formal documentation written in Object-Z. Copyright © 2005 John Wiley & Sons, Ltd.
Daniel Hoffman, Paul A. Strooper, Sarah Wilkin
Softw. Test. Verification Reliab.1
2003 Tool Support for Generating Passive C++ Test Oracles from Object-Z Specifications
abstract
A test oracle provides a means for determining whether an implementation behaves according to its specification. A passive test oracle checks that the correct behaviour has been implemented, but does not implement the behaviour itself. In previous work, we have presented a method that allows us to derive passive C++ test oracles from formal specifications written in Object-Z. We describe the "Warlock" prototype tool that supports the method. Warlock is built on top of an existing Object-Z type checker and generates oracle code for a substantial subset of the Object-Z language. We describe the architecture of Warlock and its application to a number of Object-Z specifications. We also discuss its current limitations.
Jason McDonald, Paul A. Strooper, Daniel Hoffman
APSEC3
2003 API documentation with executable examples
Daniel Hoffman, Paul A. Strooper
J. Syst. Softw.1
2003 Tool Support for Testing Concurrent Java Components
abstract
Concurrent programs are hard to test due to the inherent nondeterminism. This paper presents a method and tool support for testing concurrent Java components. Tool support is offered through ConAn (Concurrency Analyser), a tool for generating drivers for unit testing Java classes that are used in a multithreaded context. To obtain adequate controllability over the interactions between Java threads, the generated driver contains threads that are synchronized by a clock. The driver automatically executes the calls in the test sequence in the prescribed order and compares the outputs against the expected outputs specified in the test sequence. The method and tool are illustrated in detail on an asymmetric producer-consumer monitor. Their application to testing over 20 concurrent components, a number of which are sourced from industry and were found to contain faults, is presented and discussed.
Brad Long, Daniel Hoffman, Paul A. Strooper
IEEE Trans. Software Eng.2
2002 Data Coverage Testing of Programs for Container Classes
abstract
For the testing of container classes and the algorithms or programs that operate on the data in a container, these data have the property of being homogeneous throughout the container. We have developed an approach for this situation called data coverage testing, where automated test generation can systematically generate increasing test data size. Given a program and a test model, it can be theoretically shown that there exists a sufficiently large test data set size N, such that testing with a data set size larger than N does not detect more faults. A number of experiments have been conducted using a set of C++ STL programs, comparing data coverage testing with two other testing strategies: statement coverage and random generation. These experiments validate the theoretical analysis for data coverage, confirming the predicted sufficiently large N for each program.
Ponrudee Netisopakul, Lee J. White, John Morris, Daniel Hoffman
ISSRE4
2002 A framework for table driven testing of Java classes
abstract
Abstract With the advent of object‐oriented languages and the portability of Java, the development and use of class libraries has become widespread. Effective class reuse depends on class reliability which in turn depends on thorough testing. This paper describes a class testing approach based on modeling each test case with a tuple and then generating large numbers of tuples to thoroughly cover an input space with many interesting combinations of values. The testing approach is supported by the Roast framework for the testing of Java classes. Roast provides automated tuple generation based on boundary values, unit operations that support driver standardization, and test case templates used for code generation. Roast produces thorough, compact test drivers with low development and maintenance cost. The framework and tool support are illustrated on a number of non‐trivial classes, including a graphical user interface policy manager. Quantitative results are presented to substantiate the practicality and effectiveness of the approach. Copyright © 2002 John Wiley & Sons, Ltd.
Nigel Daley, Daniel Hoffman, Paul A. Strooper
Softw. Pract. Exp.2
2001 David L. Parnas Symposium
Daniel Hoffman
ICSE1
2001 A Concurrency Test Tool for Java Monitors
abstract
The Java programming language supports monitors. Monitor implementations, like other concurrent programs, are hard to test due to the inherent non-determinism. This paper presents the ConAn (Concurrency Analyser) tool for generating drivers for the testing of Java monitors. To obtain adequate controllability over the interactions between Java threads, the generated driver contains processes that are synchronized by a clock. The driver automatically executes the calls in the test sequence in the prescribed order and compares the outputs against the expected outputs specified in the test sequence. The method and tool are illustrated on an asymmetric producer-consumer monitor and their application to two other monitors is discussed.
Brad Long, Daniel Hoffman, Paul A. Strooper
ASE2
2000 Software product lines: a case study
abstract
A software product line is a family of products that share common features to meet the needs of a market area. Systematic processes have been developed to dramatically reduce the cost of a product line. Such product-line engineering processes have proven practical and effective in industrial use, but are not widely understood. The Family-Oriented Abstraction, Specification and Translation (FAST) process has been used successfully at Lucent Technologies in over 25 domains, providing productivity improvements of as much as four to one. In this paper, we show how to use FAST to document precisely the key abstractions in a domain, exploit design patterns in a generic product-line architecture, generate documentation and Java code, and automate testing to reduce costs. The paper is based on a detailed case study covering all aspects from domain analysis through testing. Copyright © 2000 John Wiley & Sons, Ltd.
Mark A. Ardis, Nigel Daley, Daniel Hoffman, Harvey P. Siy, David M. Weiss 0001
Softw. Pract. Exp.3
2000 State Generation and Automated Class Testing
abstract
The maturity of object-oriented methods has led to the wide availability of container classes: classes that encapsulate classical data structures and algorithms. Container classes are included in the C++ and Java standard libraries, and in many proprietary libraries. The wide availability and use of these classes makes reliability important, and testing plays a central role in achieving that reliability. The large number of cases necessary for thorough testing of container classes makes automated testing essential. This paper presents a novel approach for automated testing of container classes based on combinatorial algorithms for state generation. The approach is illustrated with black-box and white-box test drivers for a class implemented with the red–black tree data structure, used widely in industry and, in particular, in the C++ Standard Template Library. The white-box driver is based on a new algorithm for red–black tree generation. The drivers are evaluated experimentally, providing quantitative measures of their effectiveness in terms of block and path coverage. The results clearly show that the approach is affordable in terms of development cost and execution time, and effective with respect to coverage achieved. The results also provide insight into the relative advantages of black-box and white-box drivers, and into the difficult problem of infeasible paths. Copyright © 2000 John Wiley & Sons, Ltd.
Thomas Ball 0001, Daniel Hoffman, Frank Ruskey, Richard Webber, Lee J. White
Softw. Test. Verification Reliab.2
1999 Boundary Values and Automated Component Testing
abstract
Structural coverage approaches to software testing are mature, having been thoroughly studied for decades. Significant tool support, in the form of instrumentation for statement or branch coverage, is available in commercial compilers. While structural coverage is sensitive to which code structures are covered, it is insensitive to the values of the variables when those structures are executed. Data coverage approaches, e.g. boundary value coverage, are far less mature. They are known to practitioners mostly as a few useful heuristics with very little support for automation. Because of its sensitivity to variable values, data coverage has significant potential, especially when used in combination with structural coverage. This paper generalizes the traditional notion of boundary coverage, and formalizes it with two new data coverage measures. These measures are used to generate test cases automatically and from these, sophisticated test suites for functions from the C++ Standard Template Library. Finally, the test suites are evaluated with respect to both structural coverage and discovery of seeded faults. Copyright © 1999 John Wiley & Sons, Ltd.
Daniel Hoffman, Paul A. Strooper, Lee J. White
Softw. Test. Verification Reliab.1
1998 Programmatic Testing of the Standard Template Library Containers
abstract
We describe part of an STL conformance test suite under development. Test suites for all of the STL containers have been written, demonstrating the feasibility of thorough and highly automated testing of industrial component libraries. We describe affordable test suites that provide good code and boundary value coverage, including the thousands of cases that naturally occur from combinations of boundary values. We show how two simple oracles can provide fully automated output checking for all the containers. We refine the traditional categories of black-box and white-box testing to specification-based, implementation-based and implementation-dependent testing, and show how these three categories highlight the key cost/thoroughness trade-offs.
Jason McDonald, Daniel Hoffman, Paul A. Strooper
ASE2
1997 ClassBench: A Framework for Automated Class Testing
abstract
In contrast to the explosion of activity in object-oriented design and programming, little attention has been given to object testing. We present a novel approach to automated testing designed especially for collection classes. In the ClassBench methodology, a testgraph partially models the states and transitions of the Class-Under-Test (CUT) state/transition graph. To determine the expected behavior for the test cases generated from the testgraph, the tester develops an oracle class, providing essentially the same operations as the CUT but supporting only the testgraph states and transitions. Surprisingly thorough testing is achievable with simple testgraphs and oracles. The ClassBench framework supports the tester by providing a testgraph editor, automated testgraph traversal, and a variety of utility classes. Test suites can be easily configured for regression testing–where many test cases are run–and debugging–where a few test cases are selected to isolate the bug. We present the ClassBench methodology and framework in detail, illustrated on both simple examples and on test suites from commercial collection class libraries. © 1997 John Wiley & Sons, Ltd.
Daniel Hoffman, Paul A. Strooper
Softw. Pract. Exp.1
1995 State Abstraction and Modular Software Development
abstract
article Free Access Share on State abstraction and modular software development Authors: Daniel Hoffman University of Victoria, Department of Computer Science, P.O. Box 3055, Victoria, B. C., V8W 3P6 Canada University of Victoria, Department of Computer Science, P.O. Box 3055, Victoria, B. C., V8W 3P6 CanadaView Profile , Paul Strooper University of Queensland, Department of Computer Science, St. Lucia, Qld. 4072, Australia University of Queensland, Department of Computer Science, St. Lucia, Qld. 4072, AustraliaView Profile Authors Info & Claims ACM SIGSOFT Software Engineering NotesVolume 20Issue 4Oct. 1995 pp 53–61https://doi.org/10.1145/222132.222139Published:01 October 1995Publication History 4citation1,735DownloadsMetricsTotal Citations4Total Downloads1,735Last 12 Months13Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF
Daniel Hoffman, Paul A. Strooper
SIGSOFT FSE1
1994 Automated class testing: methods and experience
abstract
In contrast to the explosion of activity in object-oriented design and programming, little attention has been given to object testing. In our approach, a driver class and an oracle class are developed for each class-under-test (CUT). The driver class is based on a test-graph which partially models the CUT as a state machine, but with vastly fewer states and transitions. The oracle class provides essentially the same operations as the CUT, but supports only the testgraph states and transitions. Surprisingly thorough testing is achievable with simple testgraphs and oracles. The key is designing the two together, to avoid tests for which input generation and output checking are unaffordable. We summarize recent experience with the testgraphs framework, including handling of operations on pairs of objects and the application of testgraphs to test part of the testgraphs implementation.>
Daniel Hoffman, Jonathan Smillie, Paul A. Strooper
APSEC1
1994 Inspecting Module Interface Specifications
abstract
Abstract Despite dramatic changes in computing in the two decades since the term software engineering was coined, problems of deficient quality and unmanageable costs continue to afflict the software industry. Improvements in the software engineering process are vital to bringing software quality and costs under control. Module interface specification is a mature software engineering technology that, like many other proposed methodological improvements, has not significantly penetrated industrial practice. The inspection technique is well accepted for dealing with program code and pseudo‐code, but its potential for application to other work products is largely unrealized. This paper describes a successful pilot project in jointly transferring these two technologies to the software workplace. A central theme of the project was purposeful customization of the technology to a particular industrial setting. Such adaptation is important for success in the notoriously difficult process of diffusing software engineering methodology in industry.
Ann Jackson, Daniel Hoffman
Softw. Test. Verification Reliab.2
1991 Automated Module Testing in Prolog
abstract
Tools and techniques for writing scripts in Prolog that automatically test modules implemented in C are presented. Both the input generation and the test oracle problems are addressed, focusing on a balance between the adequacy of the test inputs and the cost of developing the output oracle. The authors investigate automated input generation according to functional testing, random testing, and a novel approach based on trace invariants. For each input generation scheme, a mechanism for generating the expected outputs has been developed. The methods are described and illustrated in detail. Script development and maintenance costs appear to be reasonable, and run-time performance appears to be acceptable.>
Daniel Hoffman, Paul A. Strooper
IEEE Trans. Software Eng.1
1990 On Criteria for Module Interfaces
abstract
While the benefits of modular software development are widely acknowledged, there is little agreement as to what constitutes a good module interface. Computational complexity techniques allow evaluation of algorithm time and space costs but offer no guidance in the design of the interface to an implementation. Yet, interface design decisions often have a critical effect on the development and maintenance costs of large software systems. Criteria that have led to simple, elegant interfaces are presented in detail. These criteria have been developed and refined through repeated practical application. The use of the criteria is illustrated with concrete examples.>
Daniel Hoffman
IEEE Trans. Software Eng.1
1989 A CASE study in module testing
abstract
A practical approach to module regression testing aimed at reducing the cost of test development, execution and maintenance is presented. Test cases are formally defined using a language based on module traces and a software tool is used to automatically generate test programs to apply the cases. The testing approach, language and program generator are described in detail and illustrated with a case study.>
Daniel Hoffman
ICSM1
1989 Practical Interface Specification
abstract
Abstract Although software development based on modules is now widely practiced and taught, specification of module interfaces has received far less acceptance. Languages such as Ada and Modula‐2 require an interface specification, but it is syntactic, merely listing the exported procedures and functions and their signatures. No semantic information is given, leaving the effect of each call on the return value of other calls unspecified. Module users must either guess the interface semantics or infer them from the module implementation, seriously compromising the value of the modular approach. Formal methods, such as the algebraic and trace approaches, do specify interface semantics, but have proved difficult to teach and to apply in practice. In this paper we present the software cost reduction (SCR) method for specifying the syntax and semantics of the module interface. We describe the basic approach and illustrate it on simple, but complete examples. We describe and demonstrate the additional features and techniques we have introduced to handle more complex problems. We also show the precise relationship between the SCR and trace techniques by presenting a method for converting any SCR specification to an equivalent trace specification.
Daniel Hoffman
Softw. Pract. Exp.1
1988 Trace Specifications: Methodology and Models
abstract
The authors summarize the trace specification language and present the trace specification methodology: a set of heuristics designed to make the reading and writing of complex specifications manageable. Also described is a technique for constructing formal, executable models from specifications written using the methodology. These models are useful as proof of specification consistency and as executable prototypes. Fully worked examples of the methodology and the model building techniques are included.>
Daniel Hoffman, Richard T. Snodgrass
IEEE Trans. Software Eng.1
1985 The Trace Specification of Communications Protocols
abstract
A methodology for the formal specification of communications protocols is described. Communications protocol software offers special specification problems, because typically such software connects computers which are widely distributed geographically and differ in model, manufacturer and operating system. The specification method discussed is a modified version of traces, which were originally developed as a general technique for software specification. The author first describes the trace language and presents several examples. He then describes the trace methodology, illustrated with a specification of Stenning's protocol. He summarizes his experience of using the methodology to write specifications of major portions of two commercial standards: the Advanced Data Communications Control Protocol (ADCCP) and the Internet Protocol (IP). It is concluded that traces are a feasible technique for formal specification of communications protocols.
Daniel Hoffman
IEEE Trans. Computers1