@conference {12387,
	title = {Porting DSP applications across design tools using the dataflow interchange format},
	booktitle = {Rapid System Prototyping, 2005. (RSP 2005). The 16th IEEE International Workshop on},
	year = {2005},
	month = {2005/06//},
	pages = {40 - 46},
	abstract = {Modeling DSP applications through coarse-grain dataflow graphs is popular in the DSP design community, and a growing set of rapid prototyping tools support such dataflow semantics. Since different tools may be suitable for different phases or generations of a design, it is often desirable to migrate a dataflow-based application model from one prototyping tool to another. Two critical problems in transferring dataflow-based designs across different prototyping tools are the lack of a vendor-independent language for DSP-oriented dataflow graphs, and the lack of an efficient porting methodology. In our previous work, the dataflow interchange format (DIF) (C. Hsu et al., 2004) has been developed as a standard language to specify mixed-grain dataflow models for DSP systems. This paper presents the augmentation of the DIF infrastructure with a systematic porting approach that integrates DIF tightly with the specific exporting and importing mechanisms that interface DIF to specific DSP design tools. In conjunction with this porting mechanism, this paper also introduces a novel language, called the actor interchange format (AIF), for transferring relevant information pertaining to DSP library components across different tools. Through a case study of a synthetic aperture radar application, we demonstrate the high degree of automation offered by our DIF-based porting approach.},
	keywords = {actor interchange format, coarse-grain dataflow graph, data flow analysis, data flow graphs, dataflow interchange format, dataflow model, dataflow semantic, DSP application, DSP design tool, DSP library component, electronic data interchange, formal specification, rapid prototyping tool, Signal processing, software prototyping, Specification languages, vendor-independent language},
	doi = {10.1109/RSP.2005.39},
	author = {Hsu,C.-J. and Bhattacharyya, Shuvra S.}
}
@article {15474,
	title = {Studying the fault-detection effectiveness of GUI test cases for rapidly evolving software},
	journal = {Software Engineering, IEEE Transactions on},
	volume = {31},
	year = {2005},
	month = {2005/10//},
	pages = {884 - 896},
	abstract = {Software is increasingly being developed/maintained by multiple, often geographically distributed developers working concurrently. Consequently, rapid-feedback-based quality assurance mechanisms such as daily builds and smoke regression tests, which help to detect and eliminate defects early during software development and maintenance, have become important. This paper addresses a major weakness of current smoke regression testing techniques, i.e., their inability to automatically (re)test graphical user interfaces (GUIs). Several contributions are made to the area of GUI smoke testing. First, the requirements for GUI smoke testing are identified and a GUI smoke test is formally defined as a specialized sequence of events. Second, a GUI smoke regression testing process called daily automated regression tester (DART) that automates GUI smoke testing is presented. Third, the interplay between several characteristics of GUI smoke test suites including their size, fault detection ability, and test oracles is empirically studied. The results show that: 1) the entire smoke testing process is feasible in terms of execution time, storage space, and manual effort, 2) smoke tests cannot cover certain parts of the application code, 3) having comprehensive test oracles may make up for not having long smoke test cases, and 4) using certain oracles can make up for not having large smoke test suites.},
	keywords = {daily automated regression tester, Fault diagnosis, fault-detection, formal specification, formal verification, Graphical user interfaces, GUI test cases, program testing, quality assurance mechanism, rapidly evolving software, smoke regression testing technique, software development, software fault tolerance, Software maintenance, software prototyping, Software quality, test oracles},
	isbn = {0098-5589},
	doi = {10.1109/TSE.2005.117},
	author = {Memon, Atif M. and Xie,Q.}
}
@conference {15466,
	title = {ASPIRE: automated systematic protocol implementation robustness evaluation},
	booktitle = {Software Engineering Conference, 2004. Proceedings. 2004 Australian},
	year = {2004},
	month = {2004///},
	pages = {241 - 250},
	abstract = {Network protocol implementations are susceptible to problems caused by their lack of ability to handle invalid inputs. We present ASPIRE: automated systematic protocol implementation robustness evaluation, an automated approach to pro-actively test protocol implementations by observing their responses to faulty protocol data units (PDUs) or messages. In contrast to existing approaches, we sample the faulty PDU space in a systematic manner, thus allowing us to evaluate protocol implementations in the face of a wider variety of faulty PDUs. We use a pruning strategy to reduce, from exponential, the size of the faulty PDU set to polynomial in the number of fields of a PDU. We have implemented the ASPIRE algorithms and evaluated them on implementations of HTTP (Apache, Google Web Server (GWS), and Microsoft IIS) and SMTP (Sendmail and Microsoft Exchange) protocols. Our results show that Apache, GWS, and IIS, although implementing the same protocol specification, behave differently on faulty HTTP PDUs; Sendmail and exchange are different in handling our faulty SMTP PDUs.},
	keywords = {algorithm, ASPIRE, automated systematic protocol, automated testing, fault tolerant computing, faulty PDU, formal specification, HTTP, implementation robustness evaluation, Internet, network protocol, protocol data unit, protocol specification, robustness testing, SMTP protocol, stateful protocols, stateless protocols, Transport protocols},
	doi = {10.1109/ASWEC.2004.1290477},
	author = {Vasan,Arunchandar and Memon, Atif M.}
}
@conference {18676,
	title = {Formal specification and verification of a group membership protocol for an intrusion-tolerant group communication system},
	year = {2002},
	month = {2002/12//},
	pages = {9 - 18},
	abstract = {We describe a group membership protocol that is part of an intrusion-tolerant group communication system, and present an effort to use formal tools to model and validate our protocol. We describe in detail the most difficult part of the validation exercise, which was the determination of the right level of abstraction of the protocol for formally specifying the protocol. The validation exercise not only formally showed that the protocol satisfies its correctness claims, but also provided information that will help us make the protocol more efficient without violating correctness.},
	keywords = {computer network reliability, distributed processing, distributed systems, fault tolerant computing, formal specification, formal verification, group membership protocol, intrusion-tolerant group communication system, PROMELA, Protocols},
	doi = {10.1109/PRDC.2002.1185613},
	author = {Ramasamy,H. V. and Michel Cukier and Sanders,W. H.}
}
@conference {12802,
	title = {An algebraic theory of process efficiency},
	booktitle = {, Eleventh Annual IEEE Symposium on Logic in Computer Science, 1996. LICS {\textquoteright}96. Proceedings},
	year = {1996},
	month = {1996/07/27/30},
	pages = {63 - 72},
	publisher = {IEEE},
	organization = {IEEE},
	abstract = {This paper presents a testing-based semantic theory for reasoning about the efficiency of concurrent systems as measured in terms of the amount of their internal activity. The semantic preorders are given an algebraic characterization, and their optimality is established by means of a full abstractness result. They are also shown to subsume existing bisimulation-based efficiency preorders. An example is provided to illustrate the utility of this approach},
	keywords = {algebraic characterization, algebraic specification, algebraic theory, bisimulation-based efficiency preorders, Calculus, calculus of communicating systems, Carbon capture and storage, Computer science, concurrent systems, formal logic, formal specification, full abstractness result, internal activity, optimality, process efficiency, reasoning, semantic preorders, System testing, testing-based semantic theory},
	isbn = {0-8186-7463-6},
	doi = {10.1109/LICS.1996.561304},
	author = {Natarajan,V. and Cleaveland, Rance}
}
@article {16314,
	title = {Comparing detection methods for software requirements inspections: a replicated experiment},
	journal = {IEEE Transactions on Software Engineering},
	volume = {21},
	year = {1995},
	month = {1995/06//},
	pages = {563 - 575},
	abstract = {Software requirements specifications (SRS) are often validated manually. One such process is inspection, in which several reviewers independently analyze all or part of the specification and search for faults. These faults are then collected at a meeting of the reviewers and author(s). Usually, reviewers use Ad Hoc or Checklist methods to uncover faults. These methods force all reviewers to rely on nonsystematic techniques to search for a wide variety of faults. We hypothesize that a Scenario-based method, in which each reviewer uses different, systematic techniques to search for different, specific classes of faults, will have a significantly higher success rate. We evaluated this hypothesis using a 3{\texttimes}24 partial factorial, randomized experimental design. Forty eight graduate students in computer science participated in the experiment. They were assembled into sixteen, three-person teams. Each team inspected two SRS using some combination of Ad Hoc, Checklist or Scenario methods. For each inspection we performed four measurements: (1) individual fault detection rate, (2) team fault detection rate, (3) percentage of faults first identified at the collection meeting (meeting gain rate), and (4) percentage of faults first identified by an individual, but never reported at the collection meeting (meeting loss rate). The experimental results are that (1) the Scenario method had a higher fault detection rate than either Ad Hoc or Checklist methods, (2) Scenario reviewers were more effective at detecting the faults their scenarios are designed to uncover, and were no less effective at detecting other faults than both Ad Hoc or Checklist reviewers, (3) Checklist reviewers were no more effective than Ad Hoc reviewers, and (4) Collection meetings produced no net improvement in the fault detection rate-meeting gains were offset by meeting losses},
	keywords = {Assembly, Computer science, Design for experiments, detection methods, Fault detection, fault detection rate, Fault diagnosis, formal specification, formal verification, Gain measurement, individual fault detection rate, Inspection, Loss measurement, nonsystematic techniques, performance evaluation, Performance gain, replicated experiment, scenario-based method, Software development management, software requirements inspections, software requirements specifications, team fault detection rate},
	isbn = {0098-5589},
	doi = {10.1109/32.391380},
	author = {Porter, Adam and Votta,L. G. and Basili, Victor R.}
}
@conference {12797,
	title = {When is {\textquoteleft}partial{\textquoteright} adequate? A logic-based proof technique using partial specifications},
	booktitle = {Logic in Computer Science, 1990. LICS {\textquoteright}90, Proceedings., Fifth Annual IEEE Symposium on e},
	year = {1990},
	month = {1990/06/04/7},
	pages = {440 - 449},
	publisher = {IEEE},
	organization = {IEEE},
	abstract = {A technique is presented for ascertaining when a (finite-state) partial process specification is adequate, in the sense of being specified enough, for contexts in which it is to be used. The method relies on the automatic generation of a modal formula from the partial specification; if the remainder of the network satisfies this formula, then any process that meets the specification is guaranteed to ensure correct behavior of the overall system. Using the results, the authors develop compositional proof rules for establishing the correctness of networks of parallel processes and illustrate their use with several examples},
	keywords = {Calculus, Carbon capture and storage, compositional proof rules, Computer science, Concurrent computing, Context, correctness, formal specification, logic-based proof technique, modal formula, parallel processes, partial process specification, partial specifications, specification adequacy, State-space methods, Technological innovation},
	isbn = {0-8186-2073-0},
	doi = {10.1109/LICS.1990.113768},
	author = {Cleaveland, Rance and Steffen,B.}
}
