EDBT 2026 Demo / reviewers in the wild / expert
Daniel Hoffman
dblp:h/DanielHoffman
· DBLP profile ↗
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
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Concurrent programming
concurrency bugs |
0.1 | 2 | 2003 | 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.1 | 2 | 2003 | 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.1 | 1 | 2005 | Blowtorch: a framework for firewall test automation · ASE 2005 |
Software testing
test generation |
0.1 | 1 | 2005 | Blowtorch: a framework for firewall test automation · ASE 2005 |
Software testing
unit testing |
0.0 | 2 | 2003 | 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.0 | 1 | 1998 | Programmatic Testing of the Standard Template Library Containers · ASE 1998 |
Software testing › test process › test design
test suite design |
0.0 | 1 | 1998 | Programmatic Testing of the Standard Template Library Containers · ASE 1998 |
Program analysis › static analysis
modular analysis |
0.0 | 1 | 1995 | State Abstraction and Modular Software Development · SIGSOFT FSE 1995 |
Program analysis › static analysis › abstract interpretation
state abstraction |
0.0 | 1 | 1995 | State Abstraction and Modular Software Development · SIGSOFT FSE 1995 |
Empirical software engineering
software engineering practice |
0.0 | 1 | 2001 | David L. Parnas Symposium · ICSE 2001 |
Software testing
automated testing |
0.0 | 1 | 1991 | Automated Module Testing in Prolog · IEEE Trans. Software Eng. 1991 |
Software testing › black-box testing
functional testing |
0.0 | 1 | 1991 | Automated Module Testing in Prolog · IEEE Trans. Software Eng. 1991 |
Software testing
random testing |
0.0 | 1 | 1991 | Automated Module Testing in Prolog · IEEE Trans. Software Eng. 1991 |
Software testing
test input generation |
0.0 | 1 | 1991 | Automated Module Testing in Prolog · IEEE Trans. Software Eng. 1991 |
Requirements engineering and software design › software architecture › architectural design
module interface design |
0.0 | 1 | 1990 | On Criteria for Module Interfaces · IEEE Trans. Software Eng. 1990 |
Software testing
test oracle |
0.0 | 1 | 1998 | Programmatic Testing of the Standard Template Library Containers · ASE 1998 |
Requirements engineering and software design › specification
executable specification |
0.0 | 1 | 1988 | Trace Specifications: Methodology and Models · IEEE Trans. Software Eng. 1988 |
Requirements engineering and software design › specification
software specification |
0.0 | 1 | 1988 | Trace Specifications: Methodology and Models · IEEE Trans. Software Eng. 1988 |
Internet architecture and protocols
protocol specification |
0.0 | 1 | 1985 | 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
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2016 | The Scale2 Multi-Network Architecture for IoT-Based Resilient CommunitiesabstractSafe 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 |
SMARTCOMP | 10 |
| 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 YouGenabstractAbstract 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 resultsabstractWireless 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 |
IWCMC | 3 |
| 2005 | Blowtorch: a framework for firewall test automationabstractFirewalls 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 |
ASE | 1 |
| 2005 | Tool support for executable documentation of Java class hierarchiesabstractWhile 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 SpecificationsabstractA 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 |
APSEC | 3 |
| 2003 | API documentation with executable examples
Daniel Hoffman, Paul A. Strooper |
J. Syst. Softw. | 1 |
| 2003 | Tool Support for Testing Concurrent Java ComponentsabstractConcurrent 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 ClassesabstractFor 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 |
ISSRE | 4 |
| 2002 | A framework for table driven testing of Java classesabstractAbstract 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 |
ICSE | 1 |
| 2001 | A Concurrency Test Tool for Java MonitorsabstractThe 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 |
ASE | 2 |
| 2000 | Software product lines: a case studyabstractA 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 TestingabstractThe 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 TestingabstractStructural 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 ContainersabstractWe 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 |
ASE | 2 |
| 1997 | ClassBench: A Framework for Automated Class TestingabstractIn 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 Developmentabstractarticle 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 FSE | 1 |
| 1994 | Automated class testing: methods and experienceabstractIn 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 |
APSEC | 1 |
| 1994 | Inspecting Module Interface SpecificationsabstractAbstract 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 PrologabstractTools 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 InterfacesabstractWhile 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 testingabstractA 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 |
ICSM | 1 |
| 1989 | Practical Interface SpecificationabstractAbstract 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 ModelsabstractThe 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 ProtocolsabstractA 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. Computers | 1 |