/branches/compiler/cSharp/ooasCompiler/doc/papers.bib - Annotate - OoasTools - MoMuT Open Source Repository

3

krennw

% This file was created with JabRef 2.5.

2

% Encoding: UTF-8

3

4

@INPROCEEDINGS{Aichernig2009b,

5

  author = {Bernhard K. Aichernig and Harald Brandl and Elisabeth J{\"o}bstl

6

	and Willibald Krenn},

7

  title = {Model-Based Mutation Testing of Hybrid Systems},

8

  booktitle = {FMCO},

9

  year = {2009},

10

  pages = {228-249},

11

  bibsource = {DBLP, http://dblp.uni-trier.de},

12

  ee = {http://dx.doi.org/10.1007/978-3-642-17071-3_12}

13

14

15

@INPROCEEDINGS{Alfaro2003,

16

  author = {Luca de Alfaro},

17

  title = {Game Models for Open Systems},

18

  booktitle = {Verification: Theory and Practice},

19

  year = {2003},

20

  pages = {269-289},

21

  bibsource = {DBLP, http://dblp.uni-trier.de},

22

  crossref = {DBLP:conf/birthday/2003manna},

23

  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2772{\&}spage=269},

24

  owner = {harald},

25

  timestamp = {2009.09.18}

26

27

28

@INPROCEEDINGS{Alur1998,

29

  author = {Rajeev Alur and Thomas A. Henzinger and Orna Kupferman and Moshe

30

	Y. Vardi},

31

  title = {Alternating Refinement Relations},

32

  booktitle = {CONCUR},

33

  year = {1998},

34

  pages = {163-178},

35

  bibsource = {DBLP, http://dblp.uni-trier.de},

36

  crossref = {DBLP:conf/concur/1998},

37

  ee = {http://link.springer.de/link/service/series/0558/bibs/1466/14660163.htm},

38

  owner = {harald},

39

  timestamp = {2009.09.18}

40

41

42

@INPROCEEDINGS{Bacherini2006,

43

  author = {Stefano Bacherini and Alessandro Fantechi and Matteo Tempestini and

44

	Niccol{\`o} Zingoni},

45

  title = {A Story About Formal Methods Adoption by a Railway Signaling Manufacturer},

46

  booktitle = {FM},

47

  year = {2006},

48

  pages = {179-189},

49

  bibsource = {DBLP, http://dblp.uni-trier.de},

50

  crossref = {DBLP:conf/fm/2006},

51

  ee = {http://dx.doi.org/10.1007/11813040_13},

52

  owner = {harald},

53

  timestamp = {2009.09.18}

54

55

56

@INPROCEEDINGS{Baker2002,

57

  author = {Paul Baker and Paul Bristow and Clive Jervis and David J. King and

58

	Bill Mitchell},

59

  title = {Automatic Generation of Conformance Tests from Message Sequence Charts},

60

  booktitle = {SAM},

61

  year = {2002},

62

  pages = {170-198},

63

  bibsource = {DBLP, http://dblp.uni-trier.de},

64

  crossref = {DBLP:conf/sam/2002},

65

  ee = {http://link.springer.de/link/service/series/0558/bibs/2599/25990170.htm},

66

  owner = {harald},

67

  timestamp = {2009.09.18}

68

69

70

@INPROCEEDINGS{Ball2006,

71

  author = {Thomas Ball and Ella Bounimova and Byron Cook and Vladimir Levin

72

	and Jakob Lichtenberg and Con McGarvey and Bohus Ondrusek and Sriram

73

	K. Rajamani and Abdullah Ustuner},

74

  title = {Thorough static analysis of device drivers},

75

  booktitle = {EuroSys},

76

  year = {2006},

77

  pages = {73-85},

78

  bibsource = {DBLP, http://dblp.uni-trier.de},

79

  crossref = {DBLP:conf/eurosys/2006},

80

  ee = {http://doi.acm.org/10.1145/1217935.1217943},

81

  owner = {harald},

82

  timestamp = {2009.09.18}

83

84

85

@INPROCEEDINGS{Bigot2003,

86

  author = {C{\'e}line Bigot and Alain Faivre and Jean-Pierre Gallois and Arnault

87

	Lapitre and David Lugato and Jean-Yves Pierron and Nicolas Rapin},

88

  title = {Automatic Test Generation with AGATHA},

89

  booktitle = {TACAS},

90

  year = {2003},

91

  pages = {591-596},

92

  bibsource = {DBLP, http://dblp.uni-trier.de},

93

  crossref = {DBLP:conf/tacas/2003},

94

  ee = {http://link.springer.de/link/service/series/0558/bibs/2619/26190591.htm},

95

  owner = {harald},

96

  timestamp = {2009.09.18}

97

98

99

@INPROCEEDINGS{Blackburn2002,

100

  author = {Mark R. Blackburn and Robert Busser and Aaron Nauman and Robert Knickerbocker

101

	and Richard Kasuda},

102

  title = {Mars Polar Lander Fault Identification Using Model-based Testing},

103

  booktitle = {ICECCS},

104

  year = {2002},

105

  pages = {163-},

106

  bibsource = {DBLP, http://dblp.uni-trier.de},

107

  crossref = {DBLP:conf/iceccs/2002},

108

  ee = {http://csdl.computer.org/comp/proceedings/iceccs/2002/1757/00/17570163abs.htm},

109

  owner = {harald},

110

  timestamp = {2009.09.18}

111

112

113

@INPROCEEDINGS{Blom2004,

114

  author = {Johan Blom and Anders Hessel and Bengt Jonsson and Paul Pettersson},

115

  title = {Specifying and Generating Test Cases Using Observer Automata},

116

  booktitle = {FATES},

117

  year = {2004},

118

  pages = {125-139},

119

  bibsource = {DBLP, http://dblp.uni-trier.de},

120

  crossref = {DBLP:conf/fates/2004},

121

  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3395{\&}spage=125},

122

  owner = {harald},

123

  timestamp = {2009.09.18}

124

125

126

@INPROCEEDINGS{Blom2003,

127

  author = {Johan Blom and Bengt Jonsson},

128

  title = {Automated test generation for industrial Erlang applications},

129

  booktitle = {Erlang Workshop},

130

  year = {2003},

131

  pages = {8-14},

132

  bibsource = {DBLP, http://dblp.uni-trier.de},

133

  crossref = {DBLP:conf/erlang/2003},

134

  ee = {http://doi.acm.org/10.1145/940880.940882},

135

  owner = {harald},

136

  timestamp = {2009.09.18}

137

138

139

@INPROCEEDINGS{Bohnenkamp2005,

140

  author = {Henrik C. Bohnenkamp and Axel Belinfante},

141

  title = {Timed Testing with TorX},

142

  booktitle = {FM},

143

  year = {2005},

144

  pages = {173-188},

145

  bibsource = {DBLP, http://dblp.uni-trier.de},

146

  crossref = {DBLP:conf/fm/2005},

147

  ee = {http://dx.doi.org/10.1007/11526841_13},

148

  owner = {harald},

149

  timestamp = {2009.09.18}

150

151

152

@INPROCEEDINGS{Boonstoppel2008,

153

  author = {Peter Boonstoppel and Cristian Cadar and Dawson R. Engler},

154

  title = {RWset: Attacking Path Explosion in Constraint-Based Test Generation},

155

  booktitle = {TACAS},

156

  year = {2008},

157

  pages = {351-366},

158

  bibsource = {DBLP, http://dblp.uni-trier.de},

159

  crossref = {DBLP:conf/tacas/2008},

160

  ee = {http://dx.doi.org/10.1007/978-3-540-78800-3_27},

161

  owner = {harald},

162

  timestamp = {2009.09.18}

163

164

165

@INPROCEEDINGS{Bozga2004,

166

  author = {Marius Bozga and Susanne Graf and Ileana Ober and Iulian Ober and

167

	Joseph Sifakis},

168

  title = {The IF Toolset},

169

  booktitle = {SFM},

170

  year = {2004},

171

  pages = {237-267},

172

  bibsource = {DBLP, http://dblp.uni-trier.de},

173

  crossref = {DBLP:conf/sfm/2004},

174

  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3185{\&}spage=237},

175

  owner = {harald},

176

  timestamp = {2009.09.18}

177

178

179

@INPROCEEDINGS{Brandl2008c,

180

  author = {Harald Brandl and Gordon Fraser and Franz Wotawa},

181

  title = {Coverage-based Testing Using Qualitative Reasoning Models},

182

  booktitle = {SEKE},

183

  year = {2008},

184

  pages = {393-398},

185

  bibsource = {DBLP, http://dblp.uni-trier.de},

186

  crossref = {DBLP:conf/seke/2008}

187

188

189

@INPROCEEDINGS{Braspenning,

190

  author = {N.C.W.M. Braspenning and J.M. van de Mortel-Fronczak and H.A.J. Neerhof

191

	and J.E. Rooda},

192

  title = {Model-based integration and testing in practice},

193

  booktitle = {Tangram: Model-based integration and testing of complex high-tech

194

	systems},

195

  note = {chapter 7},

196

  crossref = {Tangram2007},

197

  owner = {harald},

198

  timestamp = {2009.09.18}

199

200

201

@INPROCEEDINGS{Brucker2009,

202

  author = {Achim D. Brucker and Burkhart Wolff},

203

  title = {hol-TestGen},

204

  booktitle = {FASE},

205

  year = {2009},

206

  pages = {417-420},

207

  bibsource = {DBLP, http://dblp.uni-trier.de},

208

  crossref = {DBLP:conf/fase/2009},

209

  ee = {http://dx.doi.org/10.1007/978-3-642-00593-0_28},

210

  owner = {harald},

211

  timestamp = {2009.09.18}

212

213

214

@INPROCEEDINGS{Brucker2004,

215

  author = {Achim D. Brucker and Burkhart Wolff},

216

  title = {Symbolic Test Case Generation for Primitive Recursive Functions},

217

  booktitle = {FATES},

218

  year = {2004},

219

  pages = {16-32},

220

  bibsource = {DBLP, http://dblp.uni-trier.de},

221

  crossref = {DBLP:conf/fates/2004},

222

  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3395{\&}spage=16},

223

  owner = {harald},

224

  timestamp = {2009.09.18}

225

226

227

@INPROCEEDINGS{Cadar2006,

228

  author = {Cristian Cadar and Vijay Ganesh and Peter M. Pawlowski and David

229

	L. Dill and Dawson R. Engler},

230

  title = {EXE: automatically generating inputs of death},

231

  booktitle = {ACM Conference on Computer and Communications Security},

232

  year = {2006},

233

  pages = {322-335},

234

  bibsource = {DBLP, http://dblp.uni-trier.de},

235

  crossref = {DBLP:conf/ccs/2006usa},

236

  ee = {http://doi.acm.org/10.1145/1180405.1180445},

237

  owner = {harald},

238

  timestamp = {2009.09.18}

239

240

241

@INPROCEEDINGS{Calame2006,

242

  author = {Jens R. Calame and Nicolae Goga and Natalia Ioustinova and Jaco van

243

	de Pol},

244

  title = {TTCN-3 Testing of Hoorn-Kersenboogerd Railway Interlocking},

245

  booktitle = {CCECE},

246

  year = {2006},

247

  pages = {620-623},

248

  bibsource = {DBLP, http://dblp.uni-trier.de},

249

  crossref = {DBLP:conf/ccece/2006},

250

  ee = {http://dx.doi.org/10.1109/CCECE.2006.277762},

251

  owner = {harald},

252

  timestamp = {2009.09.18}

253

254

255

@INPROCEEDINGS{Caspi2003,

256

  author = {Paul Caspi and Adrian Curic and Aude Maignan and Christos Sofronis

257

	and Stavros Tripakis},

258

  title = {Translating Discrete-Time Simulink to Lustre},

259

  booktitle = {EMSOFT},

260

  year = {2003},

261

  pages = {84-99},

262

  bibsource = {DBLP, http://dblp.uni-trier.de},

263

  crossref = {DBLP:conf/emsoft/2003},

264

  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2855{\&}spage=84},

265

  owner = {harald},

266

  timestamp = {2009.09.18}

267

268

269

@INPROCEEDINGS{Cheon2007a,

270

  author = {Yoonsik Cheon},

271

  title = {Automated Random Testing to Detect Specification-Code Inconsistencies},

272

  booktitle = {SETP},

273

  year = {2007},

274

  pages = {112-119},

275

  bibsource = {DBLP, http://dblp.uni-trier.de},

276

  crossref = {DBLP:conf/setp/2007},

277

  owner = {harald},

278

  timestamp = {2009.09.18}

279

280

281

@INPROCEEDINGS{Cheon2007,

282

  author = {Yoonsik Cheon and Carlos E. Rubio-Medrano},

283

  title = {Random Test Data Generation for Java Classes Annotated with JML Specifications},

284

  booktitle = {Software Engineering Research and Practice},

285

  year = {2007},

286

  pages = {385-391},

287

  bibsource = {DBLP, http://dblp.uni-trier.de},

288

  crossref = {DBLP:conf/serp/2007-2},

289

  owner = {harald},

290

  timestamp = {2009.09.18}

291

292

293

@INPROCEEDINGS{Clarke2002,

294

  author = {Duncan Clarke and Thierry J{\'e}ron and Vlad Rusu and Elena Zinovieva},

295

  title = {STG: A Symbolic Test Generation Tool},

296

  booktitle = {TACAS},

297

  year = {2002},

298

  pages = {470-475},

299

  bibsource = {DBLP, http://dblp.uni-trier.de},

300

  crossref = {DBLP:conf/tacas/2002},

301

  ee = {http://link.springer.de/link/service/series/0558/bibs/2280/22800470.htm},

302

  owner = {harald},

303

  timestamp = {2009.09.18}

304

305

306

@INPROCEEDINGS{Constant2007,

307

  author = {Camille Constant and Bertrand Jeannet and Thierry J{\'e}ron},

308

  title = {Automatic Test Generation from Interprocedural Specifications},

309

  booktitle = {TestCom/FATES},

310

  year = {2007},

311

  pages = {41-57},

312

  bibsource = {DBLP, http://dblp.uni-trier.de},

313

  crossref = {DBLP:conf/pts/2007},

314

  ee = {http://dx.doi.org/10.1007/978-3-540-73066-8_4},

315

  owner = {harald},

316

  timestamp = {2009.09.18}

317

318

319

@INPROCEEDINGS{Csallner2008,

320

  author = {Christoph Csallner and Nikolai Tillmann and Yannis Smaragdakis},

321

  title = {DySy: dynamic symbolic execution for invariant inference},

322

  booktitle = {ICSE},

323

  year = {2008},

324

  pages = {281-290},

325

  bibsource = {DBLP, http://dblp.uni-trier.de},

326

  crossref = {DBLP:conf/icse/2008},

327

  ee = {http://doi.acm.org/10.1145/1368088.1368127},

328

  owner = {harald},

329

  timestamp = {2009.09.18}

330

331

332

@INPROCEEDINGS{Dauchy1991,

333

  author = {Pierre Dauchy and Bruno Marre},

334

  title = {Test Data Selection From Algebraic Specifications: Application to

335

	an Automatic Subway Module},

336

  booktitle = {ESEC},

337

  year = {1991},

338

  pages = {80-100},

339

  bibsource = {DBLP, http://dblp.uni-trier.de},

340

  crossref = {DBLP:conf/esec/1991},

341

  owner = {harald},

342

  timestamp = {2009.09.18}

343

344

345

@INPROCEEDINGS{Dulz2003,

346

  author = {Winfried Dulz and Fenhua Zhen},

347

  title = {MaTeLo - Statistical Usage Testing by Annotated Sequence Diagrams,

348

	Markov Chains and TTCN-3},

349

  booktitle = {QSIC},

350

  year = {2003},

351

  pages = {336-342},

352

  bibsource = {DBLP, http://dblp.uni-trier.de},

353

  crossref = {DBLP:conf/qsic/2003},

354

  ee = {http://csdl.computer.org/comp/proceedings/qsic/2003/2015/00/20150336abs.htm},

355

  owner = {harald},

356

  timestamp = {2009.09.18}

357

358

359

@INPROCEEDINGS{Faivre2007,

360

  author = {Alain Faivre and Christophe Gaston and Pascale Le Gall},

361

  title = {Symbolic Model Based Testing for Component Oriented Systems},

362

  booktitle = {TestCom/FATES},

363

  year = {2007},

364

  pages = {90-106},

365

  bibsource = {DBLP, http://dblp.uni-trier.de},

366

  crossref = {DBLP:conf/pts/2007},

367

  ee = {http://dx.doi.org/10.1007/978-3-540-73066-8_7},

368

  owner = {harald},

369

  timestamp = {2009.09.18}

370

371

372

@INPROCEEDINGS{Fritzson1998,

373

  author = {Peter Fritzson},

374

  title = {Modelica - A Language for Equation-Based Physical Modeling and High

375

	Performance Simulation},

376

  booktitle = {PARA},

377

  year = {1998},

378

  pages = {149-160},

379

  bibsource = {DBLP, http://dblp.uni-trier.de},

380

  crossref = {DBLP:conf/para/1998},

381

  owner = {harald},

382

  timestamp = {2009.09.18}

383

384

385

@INPROCEEDINGS{Garavel2007,

386

  author = {Hubert Garavel and Radu Mateescu and Fr{\'e}d{\'e}ric Lang and Wendelin

387

	Serwe},

388

  title = {CADP 2006: A Toolbox for the Construction and Analysis of Distributed

389

	Processes},

390

  booktitle = {CAV},

391

  year = {2007},

392

  pages = {158-163},

393

  bibsource = {DBLP, http://dblp.uni-trier.de},

394

  crossref = {DBLP:conf/cav/2007},

395

  ee = {http://dx.doi.org/10.1007/978-3-540-73368-3_18},

396

  owner = {harald},

397

  timestamp = {2009.09.18}

398

399

400

@INPROCEEDINGS{Gaston2006,

401

  author = {Christophe Gaston and Pascale Le Gall and Nicolas Rapin and Assia

402

	Touil},

403

  title = {Symbolic Execution Techniques for Test Purpose Definition},

404

  booktitle = {TestCom},

405

  year = {2006},

406

  pages = {1-18},

407

  bibsource = {DBLP, http://dblp.uni-trier.de},

408

  crossref = {DBLP:conf/pts/2006},

409

  ee = {http://dx.doi.org/10.1007/11754008_1},

410

  owner = {harald},

411

  timestamp = {2009.09.18}

412

413

414

@INPROCEEDINGS{Godefroid2005,

415

  author = {Patrice Godefroid and Nils Klarlund and Koushik Sen},

416

  title = {{DART}: directed automated random testing},

417

  booktitle = {PLDI},

418

  year = {2005},

419

  pages = {213-223},

420

  bibsource = {DBLP, http://dblp.uni-trier.de},

421

  crossref = {DBLP:conf/pldi/2005},

422

  ee = {http://doi.acm.org/10.1145/1065010.1065036},

423

  owner = {harald},

424

  timestamp = {2009.09.18}

425

426

427

@INPROCEEDINGS{Goga2001,

428

  author = {Nicolae Goga},

429

  title = {Comparing TorX, Autolink, TGV and UIO Test Algorithms},

430

  booktitle = {SDL Forum},

431

  year = {2001},

432

  pages = {379-402},

433

  bibsource = {DBLP, http://dblp.uni-trier.de},

434

  crossref = {DBLP:conf/sdl/2001},

435

  ee = {http://link.springer.de/link/service/series/0558/bibs/2078/20780379.htm},

436

  owner = {harald},

437

  timestamp = {2009.09.18}

438

439

440

@INPROCEEDINGS{Hackner2008,

441

  author = {Daniel R. Hackner and Atif M. Memon},

442

  title = {Test case generator for GUITAR},

443

  booktitle = {ICSE Companion},

444

  year = {2008},

445

  pages = {959-960},

446

  bibsource = {DBLP, http://dblp.uni-trier.de},

447

  crossref = {DBLP:conf/icse/2008c},

448

  ee = {http://doi.acm.org/10.1145/1370175.1370207},

449

  owner = {harald},

450

  timestamp = {2009.09.18}

451

452

453

@INPROCEEDINGS{Hartman2004a,

454

  author = {A. Hartman and K. Nagin},

455

  title = {The AGEDIS tools for model based testing},

456

  booktitle = {ISSTA},

457

  year = {2004},

458

  pages = {129-132},

459

  bibsource = {DBLP, http://dblp.uni-trier.de},

460

  crossref = {DBLP:conf/issta/2004},

461

  ee = {http://doi.acm.org/10.1145/1007512.1007529},

462

  owner = {harald},

463

  timestamp = {2009.09.18}

464

465

466

@INPROCEEDINGS{Hessel2008,

467

  author = {Anders Hessel and Kim Guldstrand Larsen and Marius Mikucionis and

468

	Brian Nielsen and Paul Pettersson and Arne Skou},

469

  title = {Testing Real-Time Systems Using UPPAAL},

470

  booktitle = {Formal Methods and Testing},

471

  year = {2008},

472

  pages = {77-117},

473

  bibsource = {DBLP, http://dblp.uni-trier.de},

474

  crossref = {DBLP:conf/fortest/2008},

475

  ee = {http://dx.doi.org/10.1007/978-3-540-78917-8_3},

476

  owner = {harald},

477

  timestamp = {2009.09.18}

478

479

480

@INPROCEEDINGS{Hessel2006,

481

  author = {Anders Hessel and Paul Pettersson},

482

  title = {Model-Based Testing of a WAP Gateway: An Industrial Case-Study},

483

  booktitle = {FMICS/PDMC},

484

  year = {2006},

485

  pages = {116-131},

486

  bibsource = {DBLP, http://dblp.uni-trier.de},

487

  crossref = {DBLP:conf/fmics/2006},

488

  ee = {http://dx.doi.org/10.1007/978-3-540-70952-7_8},

489

  owner = {harald},

490

  timestamp = {2009.09.18}

491

492

493

@INPROCEEDINGS{Jeannet2005,

494

  author = {Bertrand Jeannet and Thierry J{\'e}ron and Vlad Rusu and Elena Zinovieva},

495

  title = {Symbolic Test Selection Based on Approximate Analysis},

496

  booktitle = {TACAS},

497

  year = {2005},

498

  pages = {349-364},

499

  bibsource = {DBLP, http://dblp.uni-trier.de},

500

  crossref = {DBLP:conf/tacas/2005},

501

  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3440{\&}spage=349},

502

  owner = {harald},

503

  timestamp = {2009.09.18}

504

505

506

@INPROCEEDINGS{Julius2007,

507

  author = {A. Agung Julius and Georgios E. Fainekos and Madhukar Anand and Insup

508

	Lee and George J. Pappas},

509

  title = {Robust Test Generation and Coverage for Hybrid Systems},

510

  booktitle = {HSCC},

511

  year = {2007},

512

  pages = {329-342},

513

  bibsource = {DBLP, http://dblp.uni-trier.de},

514

  crossref = {DBLP:conf/hybrid/2007},

515

  ee = {http://dx.doi.org/10.1007/978-3-540-71493-4_27},

516

  owner = {harald},

517

  timestamp = {2009.09.18}

518

519

520

@INPROCEEDINGS{Koch1998,

521

  author = {Beat Koch and Jens Grabowski and Dieter Hogrefe and Michael Schmitt

522

	II},

523

  title = {Autolink: A Tool for Automatic Test Generation from SDL Specifications},

524

  booktitle = {WIFT},

525

  year = {1998},

526

  pages = {114-},

527

  bibsource = {DBLP, http://dblp.uni-trier.de},

528

  crossref = {DBLP:conf/wift/1998},

529

  ee = {http://csdl.computer.org/comp/proceedings/wift/1998/0081/00/00810114abs.htm},

530

  owner = {harald},

531

  timestamp = {2009.09.18}

532

533

534

@INPROCEEDINGS{Longuet2009,

535

  author = {Delphine Longuet and Marc Aiguier},

536

  title = {Integration Testing from Structured First-Order Specifications via

537

	Deduction Modulo},

538

  booktitle = {ICTAC},

539

  year = {2009},

540

  pages = {261-276},

541

  bibsource = {DBLP, http://dblp.uni-trier.de},

542

  crossref = {DBLP:conf/ictac/2009},

543

  ee = {http://dx.doi.org/10.1007/978-3-642-03466-4_17},

544

  owner = {harald},

545

  timestamp = {2009.09.18}

546

547

548

@INPROCEEDINGS{Lugato2004,

549

  author = {David Lugato and Fr{\'e}d{\'e}ric Maraux and Yves Le Traon and V{\'e}ronique

550

	Normand and Hubert Dubois and Jean-Yves Pierron and Jean-Pierre Gallois

551

	and Cl{\'e}mentine Nebut},

552

  title = {Automated Functional Test Case Synthesis from THALES industrial Requirements},

553

  booktitle = {IEEE Real-Time and Embedded Technology and Applications Symposium},

554

  year = {2004},

555

  pages = {104-111},

556

  bibsource = {DBLP, http://dblp.uni-trier.de},

557

  crossref = {DBLP:conf/rtas/2004},

558

  ee = {http://csdl.computer.org/comp/proceedings/rtas/2004/2148/00/21480104abs.htm},

559

  owner = {harald},

560

  timestamp = {2009.09.18}

561

562

563

@INPROCEEDINGS{Marre1995,

564

  author = {Bruno Marre},

565

  title = {LOFT: A Tool for Assisting Selection of Test Data Sets from Algebraic

566

	Specifications},

567

  booktitle = {TAPSOFT},

568

  year = {1995},

569

  pages = {799-800},

570

  bibsource = {DBLP, http://dblp.uni-trier.de},

571

  crossref = {DBLP:conf/tapsoft/1995},

572

  owner = {harald},

573

  timestamp = {2009.09.18}

574

575

576

@INPROCEEDINGS{Moser2007,

577

  author = {Andreas Moser and Christopher Kr{\"u}gel and Engin Kirda},

578

  title = {Exploring Multiple Execution Paths for Malware Analysis},

579

  booktitle = {IEEE Symposium on Security and Privacy},

580

  year = {2007},

581

  pages = {231-245},

582

  bibsource = {DBLP, http://dblp.uni-trier.de},

583

  crossref = {DBLP:conf/sp/2007},

584

  ee = {http://dx.doi.org/10.1109/SP.2007.17},

585

  owner = {harald},

586

  timestamp = {2009.09.18}

587

588

589

@INPROCEEDINGS{Moura2008,

590

  author = {Leonardo Mendon\c{c}a de Moura and Nikolaj Bj{\o}rner},

591

  title = {Z3: An Efficient SMT Solver},

592

  booktitle = {TACAS},

593

  year = {2008},

594

  pages = {337-340},

595

  bibsource = {DBLP, http://dblp.uni-trier.de},

596

  crossref = {DBLP:conf/tacas/2008},

597

  ee = {http://dx.doi.org/10.1007/978-3-540-78800-3_24},

598

  owner = {harald},

599

  timestamp = {2009.09.18}

600

601

602

@INPROCEEDINGS{Nicola2005,

603

  author = {Giuseppe De Nicola and Pasquale di Tommaso and Rosaria Esposito and

604

	Francesco Flammini and Pietro Marmo and Antonio Orazzo},

605

  title = {A Grey-Box Approach to the Functional Testing of Complex Automatic

606

	Train Protection Systems},

607

  booktitle = {EDCC},

608

  year = {2005},

609

  pages = {305-317},

610

  bibsource = {DBLP, http://dblp.uni-trier.de},

611

  crossref = {DBLP:conf/edcc/2005},

612

  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3463{\&}spage=305},

613

  owner = {harald},

614

  timestamp = {2009.09.18}

615

616

617

@INPROCEEDINGS{N'unez2005,

618

  author = {Manuel N{\'u}{\~n}ez and Ismael Rodr\'{\i}guez},

619

  title = {Conformance Testing Relations for Timed Systems},

620

  booktitle = {FATES},

621

  year = {2005},

622

  pages = {103-117},

623

  bibsource = {DBLP, http://dblp.uni-trier.de},

624

  crossref = {DBLP:conf/fates/2005},

625

  ee = {http://dx.doi.org/10.1007/11759744_8},

626

  owner = {harald},

627

  timestamp = {2009.09.18}

628

629

630

@INPROCEEDINGS{Osch2006,

631

  author = {Michiel van Osch},

632

  title = {Hybrid Input-Output Conformance and Test Generation},

633

  booktitle = {FATES/RV},

634

  year = {2006},

635

  pages = {70-84},

636

  bibsource = {DBLP, http://dblp.uni-trier.de},

637

  crossref = {DBLP:conf/fates/2006},

638

  ee = {http://dx.doi.org/10.1007/11940197_5},

639

  owner = {harald},

640

  timestamp = {2009.09.18}

641

642

643

@INPROCEEDINGS{Petrenko2005,

644

  author = {Alexandre Petrenko and Nina Yevtushenko},

645

  title = {Conformance Tests as Checking Experiments for Partial Nondeterministic

646

	FSM},

647

  booktitle = {FATES},

648

  year = {2005},

649

  pages = {118-133},

650

  bibsource = {DBLP, http://dblp.uni-trier.de},

651

  crossref = {DBLP:conf/fates/2005},

652

  ee = {http://dx.doi.org/10.1007/11759744_9},

653

  owner = {harald},

654

  timestamp = {2009.09.18}

655

656

657

@INPROCEEDINGS{Rusu2000,

658

  author = {Vlad Rusu and Lydie du Bousquet and Thierry J{\'e}ron},

659

  title = {An Approach to Symbolic Test Generation},

660

  booktitle = {IFM},

661

  year = {2000},

662

  pages = {338-357},

663

  bibsource = {DBLP, http://dblp.uni-trier.de},

664

  crossref = {DBLP:conf/ifm/2000},

665

  ee = {http://link.springer.de/link/service/series/0558/bibs/1945/19450338.htm},

666

  owner = {harald},

667

  timestamp = {2009.09.18}

668

669

670

@INPROCEEDINGS{Schieferdecker2008,

671

  author = {Ina Schieferdecker and Jens Grabowski and Theofanis Vassiliou-Gioles

672

	and George Din},

673

  title = {The Test Technology TTCN-3},

674

  booktitle = {Formal Methods and Testing},

675

  year = {2008},

676

  pages = {292-319},

677

  bibsource = {DBLP, http://dblp.uni-trier.de},

678

  crossref = {DBLP:conf/fortest/2008},

679

  ee = {http://dx.doi.org/10.1007/978-3-540-78917-8_10},

680

  owner = {harald},

681

  timestamp = {2009.09.18}

682

683

684

@INPROCEEDINGS{Sen2006,

685

  author = {Koushik Sen and Gul Agha},

686

  title = {CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking

687

	Tools},

688

  booktitle = {CAV},

689

  year = {2006},

690

  pages = {419-423},

691

  bibsource = {DBLP, http://dblp.uni-trier.de},

692

  crossref = {DBLP:conf/cav/2006},

693

  ee = {http://dx.doi.org/10.1007/11817963_38},

694

  owner = {harald},

695

  timestamp = {2009.09.18}

696

697

698

@INPROCEEDINGS{Tillmann2008,

699

  author = {Nikolai Tillmann and Jonathan de Halleux},

700

  title = {Pex-White Box Test Generation for .NET},

701

  booktitle = {TAP},

702

  year = {2008},

703

  pages = {134-153},

704

  bibsource = {DBLP, http://dblp.uni-trier.de},

705

  crossref = {DBLP:conf/tap/2008},

706

  ee = {http://dx.doi.org/10.1007/978-3-540-79124-9_10},

707

  owner = {harald},

708

  timestamp = {2009.09.18}

709

710

711

@INPROCEEDINGS{Tretmans1993,

712

  author = {Jan Tretmans},

713

  title = {A Formal Approach to Conformance Testing},

714

  booktitle = {Protocol Test Systems},

715

  year = {1993},

716

  pages = {257-276},

717

  bibsource = {DBLP, http://dblp.uni-trier.de},

718

  crossref = {DBLP:conf/pts/1993},

719

  owner = {harald},

720

  timestamp = {2009.09.18}

721

722

723

@INPROCEEDINGS{Veanes2009,

724

  author = {Margus Veanes and Nikolaj Bj{\o}rner},

725

  title = {Input-Output Model Programs},

726

  booktitle = {ICTAC},

727

  year = {2009},

728

  pages = {322-335},

729

  bibsource = {DBLP, http://dblp.uni-trier.de},

730

  crossref = {DBLP:conf/ictac/2009},

731

  ee = {http://dx.doi.org/10.1007/978-3-642-03466-4_21},

732

  owner = {harald},

733

  timestamp = {2009.09.18}

734

735

736

@INPROCEEDINGS{Veanes2008,

737

  author = {Margus Veanes and Colin Campbell and Wolfgang Grieskamp and Wolfram

738

	Schulte and Nikolai Tillmann and Lev Nachmanson},

739

  title = {Model-Based Testing of Object-Oriented Reactive Systems with Spec

740

	Explorer},

741

  booktitle = {Formal Methods and Testing},

742

  year = {2008},

743

  pages = {39-76},

744

  bibsource = {DBLP, http://dblp.uni-trier.de},

745

  crossref = {DBLP:conf/fortest/2008},

746

  ee = {http://dx.doi.org/10.1007/978-3-540-78917-8_2},

747

  owner = {harald},

748

  timestamp = {2009.09.18}

749

750

751

@INPROCEEDINGS{Weiglhofer2009,

752

  author = {Martin Weiglhofer and Franz Wotawa},

753

  title = {Asynchronous Input-Output Conformance Testing},

754

  booktitle = {COMPSAC (1)},

755

  year = {2009},

756

  pages = {154-159},

757

  bibsource = {DBLP, http://dblp.uni-trier.de},

758

  crossref = {DBLP:conf/compsac/2009},

759

  ee = {http://dx.doi.org/10.1109/COMPSAC.2009.194}

760

761

762

@MISC{(OMG),

763

  author = {The Object Management Group (OMG)},

764

  title = {OMG Systems Modeling Language},

765

  owner = {harald},

766

  timestamp = {2009.09.18},

767

  url = {http://www.omgsysml.org}

768

769

770

@ARTICLE{Abrial2007,

771

  author = {Jean-Raymond Abrial},

772

  title = {Formal Methods: Theory Becoming Practice},

773

  journal = {J. UCS},

774

  year = {2007},

775

  volume = {13},

776

  pages = {619-628},

777

  number = {5},

778

  bibsource = {DBLP, http://dblp.uni-trier.de},

779

  ee = {http://www.jucs.org/jucs_13_5/formal_methods_theory_becoming},

780

  owner = {harald},

781

  timestamp = {2009.09.18}

782

783

784

@BOOK{Abrial1996,

785

  title = {The B-book: assigning programs to meaningsp},

786

  publisher = {Cambridge University Press},

787

  year = {1996},

788

  author = {J.-R. Abrial},

789

  address = {New York, NY, USA},

790

  isbn = {0-521-49619-5},

791

  owner = {harald},

792

  timestamp = {2009.09.18}

793

794

795

@TECHREPORT{Acree1979,

796

  author = {A. T. Acree and T. A. Budd and R. A. DeMillo and R. J. Lipton and

797

	F. G. Sayward},

798

  title = {Mutation Analysis},

799

  institution = {School of Information and Computer Science, Georgia Inst. of Technology,

800

	Atlanta, Ga.},

801

  year = {1979},

802

  month = {Sept.},

803

  owner = {gordon},

804

  timestamp = {2006.04.10}

805

806

807

@ARTICLE{Aichernig2006a,

808

  author = {Aichernig, Bernhard and Delgado, Carlo },

809

  title = {From Faults Via Test Purposes to Test Cases: On the Fault-Based Testing

810

	of Concurrent Systems},

811

  journal = {Fundamental Approaches to Software Engineering},

812

  year = {2006},

813

  pages = {324--338},

814

  abstract = {Fault-based testing is a technique where testers anticipate errors

815

	in a system under test in order to assess or generate test cases.

816

	The idea is to have enough test cases capable of detecting these

817

	anticipated errors. This paper presents a theory and technique for

818

	generating fault-based test cases for concurrent systems. The novel

819

	idea is to generate test purposes from faults that have been injected

820

	into a model of the system under test. Such test purposes form a

821

	specification of a more detailed test case that can detect the injected

822

	fault. The theory is based on the notion of refinement. The technique

823

	is automated using the TGV test case generator and an equivalence

824

	checker of the CADP tools. A case study of testing web servers demonstrates

825

	the practicability of the approach.},

826

  citeulike-article-id = {2637989},

827

  doi = {10.1007/11693017\_24},

828

  keywords = {bibtex-import, tug},

829

  local-url = {file://localhost/Users/michele/mogentes/bibliography/fase06.pdf},

830

  owner = {harald},

831

  posted-at = {2008-04-07 16:23:41},

832

  priority = {2},

833

  timestamp = {2009.09.18},

834

  url = {http://dx.doi.org/10.1007/11693017\_24}

835

836

837

@ARTICLE{Aichernig2003,

838

  author = {Bernhard K. Aichernig},

839

  title = {Mutation Testing in the Refinement Calculus},

840

  journal = {Formal Aspects of Computing Journal},

841

  year = {2003},

842

  volume = {15},

843

  pages = {280--295},

844

  number = {2},

845

  owner = {harald},

846

  timestamp = {2009.09.18}

847

848

849

@ARTICLE{Aichernig2001,

850

  author = {Bernhard K.~Aichernig},

851

  title = {Test-Design through Abstraction: a Systematic Approach Based on the

852

	Refinement Calculus},

853

  journal = {Journal of Universal Computer Science},

854

  year = {2001},

855

  volume = {7},

856

  pages = {710--735},

857

  number = {8},

858

  month = aug,

859

  owner = {harald},

860

  timestamp = {2009.09.18}

861

862

863

@INPROCEEDINGS{Aichernig2011,

864

  author = {Bernhard K. Aichernig and Harald Brandl and Elisabeth J\"obstl and

865

	Willibald Krenn},

866

  title = {Efficient Mutation Killers in Action},

867

  booktitle = {Proceedings of the fourth IEEE International Conference on Software

868

	Testing, Verification and Validation (ICST)},

869

  year = {2011},

870

  month = {March},

871

  note = {in press}

872

873

874

@INPROCEEDINGS{Aichernig2010a,

875

  author = {Bernhard K. Aichernig and Harald Brandl and Elisabeth J\"obstl and

876

	Willibald Krenn},

877

  title = {{UML} in Action: A Two-Layered Interpretation for Testing},

878

  booktitle = {UML\&FM},

879

  year = {2010},

880

  series = {ACM Software Engineering Notes (SEN)},

881

  note = {in press}

882

883

884

@CONFERENCE{Aichernig2009c,

885

  author = {Bernhard K. Aichernig and Harald Brandl and Willibald Krenn},

886

  title = {Qualitative Action Systems},

887

  booktitle = {ICFEM},

888

  year = {2009},

889

  editor = {Karin Breitman and Ana Cavalcanti},

890

  volume = {5885},

891

  series = {LNCS},

892

  publisher = {Springer},

893

  longbooktitle = {Formal Methods and Software Engineering, 11th International Conference

894

	on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brasil,

895

	December 9-12, 2009. Proceedings}

896

897

898

@TECHREPORT{Aichernig2009a,

899

  author = {Bernhard K. Aichernig and Harald Brandl and Willibald Krenn and Rudolf

900

	Schlatte},

901

  title = {Model-Based Test Case Generation Techniques: A Survey},

902

  institution = {Institute for Software Technology, TU Graz},

903

  year = {2009},

904

  owner = {harald},

905

  timestamp = {2010.10.31}

906

907

908

@ARTICLE{Aichernig2009,

909

  author = {Aichernig, Bernhard K. and Brandl, Harald and Wotawa, Franz},

910

  title = {Conformance Testing of Hybrid Systems with Qualitative Reasoning

911

	Models},

912

  journal = {Electron. Notes Theor. Comput. Sci.},

913

  year = {2009},

914

  volume = {253},

915

  pages = {53--69},

916

  number = {2},

917

  address = {Amsterdam, The Netherlands, The Netherlands},

918

  doi = {http://dx.doi.org/10.1016/j.entcs.2009.09.051},

919

  issn = {1571-0661},

920

  publisher = {Elsevier Science Publishers B. V.}

921

922

923

@INPROCEEDINGS{Aichernig2006,

924

  author = {Bernhard K. Aichernig and Carlo Corrales Delgado},

925

  title = {From Faults Via Test Purposes to Test Cases: On the Fault-Based Testing

926

	of Concurrent Systems.},

927

  booktitle = {Proceedings of the 9th International Conference on Fundamental Approaches

928

	to Software Engineering},

929

  year = {2006},

930

  volume = {3922},

931

  series = {LNCS},

932

  pages = {324-338},

933

  publisher = {Springer},

934

  abstract = {This paper discusses how to use a fault based approach for test purpose

935

	generation. The authors generate test purposes by generating a mutant

936

	from the specification. Therfore they apply one of 27 mutation operators

937

	to the specification. Afterwards, they generate the labeled transition

938

	systems of the specification and the mutant. By doing an equivalence

939

	check between the two LTSs the authors generate a discriminating

940

	sequence. This sequence is used as new test purpose on the specification.},

941

  comment = {p,r},

942

  file = {aichernig2006faults.pdf:aichernig2006faults.pdf:PDF},

943

  keywords = {mutation, test purpose generation, lts, refinement,},

944

  owner = {martin},

945

  timestamp = {2007.07.27}

946

947

948

@ARTICLE{Aichernig2007b,

949

  author = {Aichernig, Bernhard K. and He, Jifeng },

950

  title = {Mutation Testing in UTP},

951

  journal = {Under consideration for publication in Formal Aspects of Computing},

952

  year = {2007},

953

  abstract = {This paper presents a theory of testing that integrates into Hoare

954

	and He's Unifying Theory of Programming (UTP).We give test cases

955

	a denotational semantics by viewing them as specification predicates.

956

	This reformulation of test cases allows for relating test cases via

957

	refinement to specifications and programs. Having such a refinement

958

	order that integrates test cases, we develop a testing theory for

959

	fault-based testing. Fault-based testing uses test data designed

960

	to demonstrate the absence of a set of pre-specified faults. A well-known

961

	fault-based technique is mutation testing. In mutation testing, first,

962

	faults are injected into a program by altering (mutating) its source

963

	code. Then, test cases that can detect these errors are designed.

964

	The assumption is that other faults will be caught, too. In this

965

	paper, we apply the mutation technique to both, specifications and

966

	programs. Using our theory of testing, two new test case generation

967

	laws for detecting injected (anticipated) faults are presented: one

968

	is based on the semantic level of UTP design predicates, the other

969

	on the algebraic properties of a small programming language. Keywords:

970

	specification-based testing; fault-based testing; mutation testing;

971

	Unifying Theories of Programming; refinement calculus; algebra of

972

	programming.},

973

  citeulike-article-id = {2637991},

974

  keywords = {bibtex-import, mutation-testing, reading-group-testing, softnet, tug},

975

  local-url = {file://localhost/Users/michele/mogentes/bibliography/facj08.pdf},

976

  owner = {harald},

977

  posted-at = {2008-04-07 16:23:41},

978

  priority = {2},

979

  timestamp = {2009.09.18}

980

981

982

@INPROCEEDINGS{Aichernig2005,

983

  author = {Bernhard K. Aichernig and Percy Antonio {Pari Salas}},

984

  title = {Test Case Generation by {OCL} Mutation and Constraint Solving},

985

  booktitle = {{QSIC 2OO5}, Proceedings of the Fifth International Conference on

986

	Quality Software, Melbourne, Australia, September 19-21, 2005},

987

  year = {2005},

988

  editor = {Kai-Yuan Cai and Atsushi Ohnishi and M.F. Lau},

989

  pages = {64--71},

990

  publisher = {IEEE Computer Society Press},

991

  owner = {harald},

992

  timestamp = {2009.09.18}

993

994

995

@INPROCEEDINGS{Aichernig2007a,

996

  author = {Bernhard K. Aichernig and Bernhard Peischl and Martin Weiglhofer

997

	and Franz Wotawa},

998

  title = {Protocol Conformance Testing a {SIP} Registrar: An Industrial Application

999

	of Formal Methods},

1000

  booktitle = {Proceedings of the 5th IEEE International Conference on Software

1001

	Engineering and Formal Methods},

1002

  year = {2007},

1003

  editor = {Mike Hinchey and Tiziana Margaria},

1004

  pages = {215--224},

1005

  address = {London, UK},

1006

  publisher = {IEEE},

1007

  comment = {a},

1008

  file = {aichernig2007protocol.pdf:aichernig2007protocol.pdf:PDF},

1009

  owner = {harald},

1010

  timestamp = {2009.09.18}

1011

1012

1013

@ARTICLE{Aichernig19-20Sept.2005,

1014

  author = {Aichernig, B. K. and Salas, P. A. P. },

1015

  title = {Test case generation by OCL mutation and constraint solving},

1016

  journal = {Quality Software, 2005. (QSIC 2005). Fifth International Conference

1017

	on},

1018

  year = {19-20 Sept. 2005},

1019

  pages = {64--71},

1020

  citeulike-article-id = {2637988},

1021

  doi = {10.1109/QSIC.2005.63},

1022

  keywords = {bibtex-import, case, constraint, fault, fault-based, formal, generation,

1023

	language, languages, mutation, ocl, problem, program, programming,

1024

	satisfaction, semantics, software, solving, specification, state-based,

1025

	test, testing, theory, tolerance, tug},

1026

  local-url = {file://localhost/Users/michele/mogentes/bibliography/01579121.pdf},

1027

  owner = {harald},

1028

  posted-at = {2008-04-07 16:23:41},

1029

  priority = {2},

1030

  timestamp = {2009.09.18},

1031

  url = {http://dx.doi.org/10.1109/QSIC.2005.63}

1032

1033

1034

@INPROCEEDINGS{Aichernig2007,

1035

  author = {Aichernig, Bernhard K. and Weiglhofer, Martin and Peischl, Bernhard

1036

	and Wotawa, Franz },

1037

  title = {Test purpose generation in an industrial application},

1038

  booktitle = {A-MOST '07: Proceedings of the 3rd international workshop on Advances

1039

	in model-based testing},

1040

  year = {2007},

1041

  pages = {115--125},

1042

  address = {New York, NY, USA},

1043

  publisher = {ACM},

1044

  citeulike-article-id = {2637993},

1045

  doi = {http://doi.acm.org/10.1145/1291535.1291547},

1046

  keywords = {bibtex-import, tug},

1047

  local-url = {file://localhost/Users/michele/mogentes/bibliography/amost2007.pdf},

1048

  owner = {harald},

1049

  posted-at = {2008-04-07 16:23:41},

1050

  priority = {2},

1051

  timestamp = {2009.09.18},

1052

  url = {http://dx.doi.org/10.1145/1291535.1291547}

1053

1054

1055

@ARTICLE{Aichernig2008,

1056

  author = {Bernhard K. Aichernig and Martin Weiglhofer and Franz Wotawa},

1057

  title = {Improving Fault-based Conformance Testing},

1058

  journal = {Electronic Notes in Theoretical Computer Science},

1059

  year = {2008},

1060

  note = {to appear},

1061

  comment = {a},

1062

  file = {aichernig2008improving.pdf:aichernig2008improving.pdf:PDF},

1063

  owner = {martin},

1064

  timestamp = {2008.05.20}

1065

1066

1067

@INPROCEEDINGS{Alur1990,

1068

  author = {Rajcev Alur and Costas Courcoubetis and David Dill},

1069

  title = {Model-{C}hecking for {R}eal-{T}ime {S}ystems},

1070

  booktitle = {Proceedings of the {F}ifth {A}nnual {IEEE} {S}ymposium on {L}ogic

1071

	in {C}omputer {S}cience ({LICS} 90)},

1072

  year = {1990},

1073

  pages = {414-425},

1074

  owner = {gordon},

1075

  timestamp = {2009.09.18}

1076

1077

1078

@INPROCEEDINGS{Alur2000,

1079

  author = {Rajeev Alur and Radu Grosu and Yerang Hur and Vijay Kumar and Insup

1080

	Lee},

1081

  title = {Modular Specification of Hybrid Systems in CHARON},

1082

  booktitle = {HSCC '00: Proceedings of the Third International Workshop on Hybrid

1083

	Systems: Computation and Control},

1084

  year = {2000},

1085

  pages = {6--19},

1086

  address = {London, UK},

1087

  publisher = {Springer-Verlag},

1088

  isbn = {3-540-67259-1},

1089

  owner = {harald},

1090

  timestamp = {2009.09.18}

1091

1092

1093

@INPROCEEDINGS{Ammann1999,

1094

  author = {Paul Ammann and Paul E. Black},

1095

  title = {A {S}pecification-{B}ased {C}overage {M}etric to {E}valuate {T}est

1096

	{S}ets.},

1097

  booktitle = {{HASE} '99: The 4th {IEEE} International Symposium on High-Assurance

1098

	Systems Engineering},

1099

  year = {1999},

1100

  pages = {239--248},

1101

  address = {Washington, DC, USA},

1102

  publisher = {IEEE Computer Society},

1103

  isbn = {0-7695-0418-3},

1104

  owner = {harald},

1105

  timestamp = {2009.09.18}

1106

1107

1108

@ARTICLE{Back1988,

1109

  author = {R. J. R. Back and F. Kurki-Suonio},

1110

  title = {Distributed cooperation with action systems},

1111

  journal = {ACM Trans. Program. Lang. Syst.},

1112

  year = {1988},

1113

  volume = {10},

1114

  pages = {513--554},

1115

  number = {4},

1116

  address = {New York, NY, USA},

1117

  doi = {http://doi.acm.org/10.1145/48022.48023},

1118

  issn = {0164-0925},

1119

  owner = {harald},

1120

  publisher = {ACM},

1121

  timestamp = {2009.09.18}

1122

1123

1124

@INPROCEEDINGS{Back1983,

1125

  author = {Back, Ralph-Johan and Kurki-Suonio, Reino},

1126

  title = {Decentralization of Process Nets with Centralized Control},

1127

  booktitle = {Proceedings of the 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed

1128

	Computing},

1129

  year = {1983},

1130

  pages = {131-142},

1131

  address = {Montreal, Quebec, Canada},

1132

  organization = {ACM},

1133

  project = {actions distributed}

1134

1135

1136

@ARTICLE{Back2001,

1137

  author = {Back, Ralph-Johan and Petre, Luigia and Porres, Ivan},

1138

  title = {Continuous Action Systems as a Model for Hybrid Systems},

1139

  journal = {Nordic Journal of Computing},

1140

  year = {2001},

1141

  volume = {8},

1142

  pages = {2--21},

1143

  number = {1},

1144

  timestamp = {2009.04.01}

1145

1146

1147

@ARTICLE{Back1991,

1148

  author = {Back, Ralph-Johan and Sere, Kaisa},

1149

  title = {Stepwise Refinement of Action Systems},

1150

  journal = {Structured Programming},

1151

  year = {1991},

1152

  volume = {12},

1153

  pages = {17--30}

1154

1155

1156

@INPROCEEDINGS{Back1994,

1157

  author = {Back, Ralph-Johan and von Wright, Joakim},

1158

  title = {Trace Refinement of Action Systems},

1159

  booktitle = {CONCUR-94:Concurrency Theory},

1160

  year = {1994},

1161

  editor = {Jonsson, B and Parrow, J.},

1162

  volume = {836},

1163

  series = {Lecture Notes in Computer Science},

1164

  pages = {367-384},

1165

  address = {Uppsala, Sweden},

1166

  month = {Aug},

1167

  publisher = {Springer-Verlag}

1168

1169

1170

@BOOK{Back1998,

1171

  title = {Refinement Calculus, a Systematic Introduction},

1172

  publisher = {Springer},

1173

  year = {1998},

1174

  author = {Ralph-Johan Back and Joakim von Wright},

1175

  series = {Graduate Texts in Computer Science},

1176

  owner = {harald},

1177

  timestamp = {2009.09.18}

1178

1179

1180

@ARTICLE{Backus1978,

1181

  author = {John W. Backus},

1182

  title = {Can Programming Be Liberated From the von Neumann Style? A Functional

1183

	Style and its Algebra of Programs},

1184

  journal = {Commun. ACM},

1185

  year = {1978},

1186

  volume = {21},

1187

  pages = {613-641},

1188

  number = {8},

1189

  bibsource = {DBLP, http://dblp.uni-trier.de},

1190

  owner = {harald},

1191

  timestamp = {2009.09.18}

1192

1193

1194

@INPROCEEDINGS{Badban2006,

1195

  author = {Bahareh Badban and Martin Fr\"{a}nzle and Jan Peleska and Tino Teige},

1196

  title = {Test automation for hybrid systems},

1197

  booktitle = {SOQUA '06: Proceedings of the 3rd international workshop on Software

1198

	quality assurance},

1199

  year = {2006},

1200

  pages = {14--21},

1201

  address = {New York, NY, USA},

1202

  publisher = {ACM},

1203

  doi = {http://doi.acm.org/10.1145/1188895.1188902},

1204

  isbn = {1-59593-584-3},

1205

  location = {Portland, Oregon},

1206

  owner = {harald},

1207

  timestamp = {2009.09.18}

1208

1209

1210

@MASTERSTHESIS{Bakker2006,

1211

  author = {Elinor Bakker},

1212

  title = {Qualitative models of population dynamics},

1213

  school = {University of Amsterdam},

1214

  year = {2006},

1215

  owner = {harald},

1216

  timestamp = {2010.08.31}

1217

1218

1219

@ARTICLE{Balcer1989,

1220

  author = {M. Balcer and W. Hasling and T. Ostrand},

1221

  title = {Automatic generation of test scripts from formal test specifications},

1222

  journal = {SIGSOFT Softw. Eng. Notes},

1223

  year = {1989},

1224

  volume = {14},

1225

  pages = {210--218},

1226

  number = {8},

1227

  address = {New York, NY, USA},

1228

  doi = {http://doi.acm.org/10.1145/75309.75332},

1229

  issn = {0163-5948},

1230

  owner = {harald},

1231

  publisher = {ACM},

1232

  timestamp = {2009.09.18}

1233

1234

1235

@TECHREPORT{Ball2004,

1236

  author = {Ball, Thomas },

1237

  title = {A Theory of Predicate-Complete Test Coverage and Generation},

1238

  institution = {Microsoft Research},

1239

  year = {2004},

1240

  abstract = {Consider a program with m statements and n predicates, where the predicates

1241

	are derived from the conditional state- ments and assertions in a

1242

	program, as well as from implicit run-time safety checks. An observable

1243

	state is an evaluation of the n predicates under some state at a

1244

	program statement. The goal of predicate-complete testing (PCT) is

1245

	to cover every reachable observable state (at most m x 2n of them)

1246

	in a program. PCT coverage is a new form of coverage motivated by

1247

	the observation that certain errors in a pro- gram only can be exposed

1248

	by considering the complex depen- dences between the predicates in

1249

	a program and the state- ments whose execution they control. PCT

1250

	coverage sub- sumes many existing control-flow coverage criteria

1251

	and is incomparable to path coverage. To support the generation of

1252

	tests to achieve high PCT coverage, we show how to define an upper

1253

	bound U and lower bound L to the (unknown) set of reachable observable

1254

	states R. These bounds are constructed automatically using Boolean

1255

	(predicate) abstraction over modal transition sys- tems and can be

1256

	used to guide test generation via symbolic execution. We define a

1257

	static coverage metric as |L|/|U |, which measures the ability of

1258

	the Boolean abstraction to achieve high PCT coverage. Finally we

1259

	show how to in- crease this ratio by the addition of new predicates.},

1260

  citeulike-article-id = {2638017},

1261

  keywords = {bibtex-import},

1262

  local-url = {file://localhost/Users/michele/mogentes/bibliography/TR-2004-28.pdf},

1263

  owner = {harald},

1264

  posted-at = {2008-04-07 16:23:45},

1265

  priority = {2},

1266

  timestamp = {2009.09.18}

1267

1268

1269

@INPROCEEDINGS{BANDELJ2002,

1270

  author = {Aleksander Bandelj and Ivan Bratko and Dorian Šuc},

1271

  title = {Qualitative simulation with {CLP}},

1272

  booktitle = {In Proc. of 16th International Workshop on Qualitative Reasoning

1273

	(QR’02},

1274

  year = {2002}

1275

1276

1277

@INPROCEEDINGS{Barbey1994,

1278

  author = {S. Barbey and D. Buchs},

1279

  title = {Testing {Ada} abstract data types using formal specifications.},

1280

  booktitle = {1st Int. Eurospace-Ada-Europe Symposium},

1281

  year = {1994},

1282

  volume = {887},

1283

  series = {Lecture Notes in Computer Science},

1284

  pages = {76--89},

1285

  publisher = {Springer-Verlag},

1286

  owner = {harald},

1287

  timestamp = {2009.09.18}

1288

1289

1290

@BOOK{Barnes2003,

1291

  title = {High Integrity Software: The SPARK Approach to Safety and Security},

1292

  publisher = {Addison-Wesley Longman Publishing Co., Inc.},

1293

  year = {2003},

1294

  author = {John Barnes},

1295

  address = {Boston, MA, USA},

1296

  isbn = {0321136160},

1297

  owner = {harald},

1298

  timestamp = {2009.09.18}

1299

1300

1301

@INCOLLECTION{Barnett2005,

1302

  author = {Mike Barnett and K. Rustan M. Leino and Wolfram Schulte},

1303

  title = {The {Spec\#} Programming System: An Overview},

1304

  booktitle = {Construction and Analysis of Safe, Secure, and Interoperable Smart

1305

	Devices},

1306

  publisher = {Springer-Verlag},

1307

  year = {2005},

1308

  volume = {3362},

1309

  series = {Lecture Notes in Computer Science},

1310

  pages = {49--69},

1311

  keywords = {survey, testing},

1312

  owner = {harald},

1313

  timestamp = {2009.09.18}

1314

1315

1316

@INPROCEEDINGS{Bauer2007,

1317

  author = {Bauer, A. and Pister, M. and Tautschnig, M. },

1318

  title = {Tool-support for the analysis of hybrid systems and models},

1319

  booktitle = {Design, Automation \& Test in Europe Conference \& Exhibition, 2007.

1320

	DATE '07},

1321

  year = {2007},

1322

  pages = {1--6},

1323

  abstract = {This paper introduces a method and tool-support for the automatic

1324

	analysis and verification of hybrid and embedded control systems,

1325

	whose continuous dynamics are often modelled using MATLAB/Simulink.

1326

	The method is based upon converting system models into the uniform

1327

	input language of our efficient multi-domain constraint solving library,

1328

	ABSOLVER, which is then used for subsequent analysis. Basically,

1329

	ABSOLVER is an extensible SMT-solver which addresses mixed Boolean

1330

	and (nonlinear) arithmetic constraint problems as they appear in

1331

	the design of hybrid control systems. It allows the integration and

1332

	semantic connection of various domain specific solvers via a logical

1333

	circuit, such that almost arbitrary multi-domain constraint problems

1334

	can be formulated and solved. Its design has been tailored for extensibility,

1335

	and thus facilitates the reuse of expert knowledge, in that the most

1336

	appropriate solver for a given task can be integrated and used. As

1337

	such the only constraint over the problem domain is the capability

1338

	of the employed solvers. Our approach to systems verification has

1339

	been validated in an industrial case study using the model of a car's

1340

	steering control system. However, additional benchmarks show that

1341

	other hard instances of problems could also be solved by ABSOLVER

1342

	in respectable time, and that for some instances, ABsOLVER's approach

1343

	was the only means of solving a problem at all},

1344

  citeulike-article-id = {2721207},

1345

  doi = {10.1109/DATE.2007.364411},

1346

  journal = {Design, Automation \& Test in Europe Conference \& Exhibition, 2007.

1347

	DATE '07},

1348

  keywords = {mogentes, sat, smt, testing},

1349

  owner = {harald},

1350

  posted-at = {2008-05-05 12:40:32},

1351

  priority = {2},

1352

  timestamp = {2009.09.18},

1353

  url = {http://dx.doi.org/10.1109/DATE.2007.364411}

1354

1355

1356

@INPROCEEDINGS{Beckman2008,

1357

  author = {Nels E. Beckman and Aditya V. Nori and Sriram K. Rajamani and Robert

1358

	J. Simmons},

1359

  title = {Proofs from Tests},

1360

  booktitle = {Poceedings of the International Symposium on Software Testing and

1361

	Analysis},

1362

  year = {2008},

1363

  note = {to appear},

1364

  owner = {harald},

1365

  timestamp = {2009.09.18}

1366

1367

1368

@INPROCEEDINGS{Belinfante2010,

1369

  author = {Axel Belinfante},

1370

  title = {{JT}or{X}: A Tool for On-Line Model-Driven Test Derivation and Execution},

1371

  booktitle = {TACAS},

1372

  year = {2010},

1373

  pages = {266-270},

1374

  bibsource = {DBLP, http://dblp.uni-trier.de},

1375

  ee = {http://dx.doi.org/10.1007/978-3-642-12002-2_21}

1376

1377

1378

@INPROCEEDINGS{Belinfante2004,

1379

  author = {Axel Belinfante and Lars Frantzen and Christian Schallhart},

1380

  title = {Tools for Test Case Generation},

1381

  booktitle = {Model-Based Testing of Reactive Systems},

1382

  year = {2004},

1383

  pages = {391-438},

1384

  bibsource = {DBLP, http://dblp.uni-trier.de},

1385

  ee = {http://dx.doi.org/10.1007/11498490_18},

1386

  owner = {harald},

1387

  timestamp = {2009.09.18}

1388

1389

1390

@ARTICLE{Bernard2004,

1391

  author = {Eddy Bernard and Bruno Legeard and Xavier Luck and Fabien Peureux},

1392

  title = {Generation of test sequences from formal specifications: GSM 11-11

1393

	standard case study},

1394

  journal = {Softw., Pract. Exper.},

1395

  year = {2004},

1396

  volume = {34},

1397

  pages = {915-948},

1398

  number = {10},

1399

  bibsource = {DBLP, http://dblp.uni-trier.de},

1400

  ee = {http://dx.doi.org/10.1002/spe.597},

1401

  owner = {harald},

1402

  timestamp = {2009.09.18}

1403

1404

1405

@INPROCEEDINGS{Bernot1991a,

1406

  author = {Bernot, Gilles},

1407

  title = {Testing Against Formal Specifications: A Theoretical View},

1408

  booktitle = {TAPSOFT '91: Proceedings of the International Joint Conference on

1409

	Theory and Practice of Software Development, Volume 2: Advances in

1410

	Distributed Computing (ADC) and Colloquium on Combining Paradigms

1411

	for Software Developmemnt (CCPSD)},

1412

  year = {1991},

1413

  pages = {99--119},

1414

  address = {London, UK},

1415

  publisher = {Springer-Verlag},

1416

  isbn = {3-540-53981-6}

1417

1418

1419

@ARTICLE{Bernot1991,

1420

  author = {G. Bernot and M.-C. Gaudel and B. Marre},

1421

  title = {Software testing based on formal specifications: a theory and a tool.},

1422

  journal = {Software Engineering Journal},

1423

  year = {1991},

1424

  volume = {6},

1425

  pages = {387--405},

1426

  number = {6},

1427

  owner = {harald},

1428

  timestamp = {2009.09.18}

1429

1430

1431

@ARTICLE{Berry1992,

1432

  author = {Gerard Berry and Georges Gonthier},

1433

  title = {The Esterel Synchronous Programming Language: Design, Semantics,

1434

	Implementation},

1435

  journal = {Science of Computer Programming},

1436

  year = {1992},

1437

  volume = {19},

1438

  pages = {87-152},

1439

  number = {2},

1440

  owner = {harald},

1441

  timestamp = {2009.09.18},

1442

  url = {citeseer.ist.psu.edu/berry92esterel.html}

1443

1444

1445

@ARTICLE{Beyer2004,

1446

  author = {Beyer, Dirk and Chlipala, Adam J. and Henzinger, Thomas A. and Jhala,

1447

	Ranjit and Majumdar, Rupak },

1448

  title = {Generating Tests from Counterexamples},

1449

  journal = {icse},

1450

  year = {2004},

1451

  volume = {0},

1452

  pages = {326--335},

1453

  abstract = {We have extended the software model checker BLAST to automatically

1454

	generate test suites that guarantee full coverage with respect to

1455

	a given predicate. More precisely, given a C program and a target

1456

	predicate, BLAST determines the set  of program locations which

1457

	program execution can reach with true, and automatically generates

1458

	a set of test vectors that exhibit the truth of at all locations

1459

	in . We have used BLAST to generate test suites and to detect dead

1460

	code in C programs with up to 30 K lines of code. The analysis and

1461

	test-vector generation is fully automatic (no user intervention)

1462

	and exact (no false positives).},

1463

  address = {Los Alamitos, CA, USA},

1464

  citeulike-article-id = {2638016},

1465

  doi = {http://doi.ieeecomputersociety.org/10.1109/ICSE.2004.1317455},

1466

  keywords = {bibtex-import},

1467

  local-url = {file://localhost/Users/michele/mogentes/bibliography/2004-ICSE.Generating\_Tests\_from\_Counterexamples.pdf},

1468

  owner = {harald},

1469

  posted-at = {2008-04-07 16:23:45},

1470

  priority = {2},

1471

  publisher = {IEEE Computer Society},

1472

  timestamp = {2009.09.18},

1473

  url = {http://doi.ieeecomputersociety.org/10.1109/ICSE.2004.1317455}

1474

1475

1476

@ARTICLE{Biere2003,

1477

  author = {Armin Biere and Alessandro Cimatti and Edmund M. Clarke and Ofer

1478

	Strichman and Yunshan Zhu},

1479

  title = {Bounded model checking},

1480

  journal = {Advances in Computers},

1481

  year = {2003},

1482

  volume = {58},

1483

  pages = {118-149},

1484

  bibsource = {DBLP, http://dblp.uni-trier.de}

1485

1486

1487

@INPROCEEDINGS{Black2000,

1488

  author = {Paul E. Black and Vadim Okun and Yaacov Yesha},

1489

  title = {Mutation {O}perators for {S}pecifications},

1490

  booktitle = {Proceedings of the {F}ifteenth {IEEE} {I}nternational {C}onference

1491

	on {A}utomated {S}oftware {E}ngineering ({ASE}'00)},

1492

  year = {2000},

1493

  address = {Washington, DC, USA},

1494

  publisher = {IEEE Computer Society},

1495

  owner = {gordon},

1496

  timestamp = {2009.09.18}

1497

1498

1499

@ARTICLE{Blackburn1996,

1500

  author = {Blackburn, MR and Busser, RD},

1501

  title = {{T-VEC: a tool for developing critical systems}},

1502

  journal = {Computer Assurance, 1996. COMPASS'96,'Systems Integrity. Software

1503

	Safety. Process Security'. Proceedings of the Eleventh Annual Conference

1504

	on},

1505

  year = {1996},

1506

  pages = {237--249},

1507

  owner = {harald},

1508

  timestamp = {2009.09.18}

1509

1510

1511

@INPROCEEDINGS{Bohn2002,

1512

  author = {J. Bohn and W. Damm and J. Klose and A. Moik and H. Wittke},

1513

  title = {Modeling and validating train system applications using Statemate

1514

	and Live Sequence Charts},

1515

  booktitle = {Proceedings of the Conference on Integrated Design and Process Technology

1516

	(IDPT2002)},

1517

  year = {2002},

1518

  editor = {H. Ehrig and B. J. Kramer and A. Ertas},

1519

  owner = {harald},

1520

  timestamp = {2009.09.18},

1521

  url = {citeseer.ist.psu.edu/bohn02modeling.html}

1522

1523

1524

@INPROCEEDINGS{Bonsangue1998,

1525

  author = {Marcello M. Bonsangue and Joost N. Kok and Kaisa Sere},

1526

  title = {An Approach to Object-Orientation in Action Systems},

1527

  booktitle = {Mathematics of Program Construction, LNCS 1422},

1528

  year = {1998},

1529

  pages = {68--95},

1530

  publisher = {Springer},

1531

  owner = {wkrenn},

1532

  timestamp = {2010.02.04}

1533

1534

1535

@ARTICLE{Borras2006,

1536

  author = {Cari Borr\'as},

1537

  title = {{Overexposure of Radiation Therapy Patients in Panama: Problem Recognition

1538

	and Follow-Up Measures}},

1539

  journal = {{Rev Panam Salud Publica}},

1540

  year = {2006},

1541

  volume = {20},

1542

  pages = {173-187},

1543

  number = {2/3},

1544

  file = {:home/elisabeth/Diplomarbeit/Literatur/PDFs/panama.pdf:PDF},

1545

  keywords = {http://journal.paho.org/uploads/1162234952.pdf},

1546

  owner = {elisabeth},

1547

  timestamp = {2009.09.08},

1548

  url = {http://journal.paho.org/uploads/1162234952.pdf}

1549

1550

1551

@ARTICLE{Boug'e1985,

1552

  author = {L. Boug\'{e}},

1553

  title = {A contribution to the theory of program testing},

1554

  journal = {Theoretical Computer Science},

1555

  year = {1985},

1556

  volume = {37},

1557

  pages = {151--181},

1558

  number = {2},

1559

  owner = {harald},

1560

  timestamp = {2009.09.18}

1561

1562

1563

@PHDTHESIS{Boug'e1982,

1564

  author = {L. Boug\'{e}},

1565

  title = {Mod\'{e}lisation de la notion de test de programmes, application

1566

	\`{a} la production de jeux de test},

1567

  school = {Universit\'{e} de Paris 6},

1568

  year = {1982},

1569

  owner = {harald},

1570

  timestamp = {2009.09.18}

1571

1572

1573

@ARTICLE{Boug'e1986,

1574

  author = {L. Boug\'{e} and N. Choquet and L. Fribourg and M.-C. Gaudel},

1575

  title = {Test set generation from algebraic specifications using logic programming.},

1576

  journal = {Journal of Systems and Software},

1577

  year = {1986},

1578

  volume = {6},

1579

  pages = {343--360},

1580

  number = {4},

1581

  owner = {harald},

1582

  timestamp = {2009.09.18}

1583

1584

1585

@INPROCEEDINGS{Bouissou2008,

1586

  author = {Bouissou, Olivier and Martel, Matthieu},

1587

  title = {Abstract interpretation of the physical inputs of embedded programs},

1588

  booktitle = {VMCAI'08: Proceedings of the 9th international conference on Verification,

1589

	model checking, and abstract interpretation},

1590

  year = {2008},

1591

  pages = {37--51},

1592

  address = {Berlin, Heidelberg},

1593

  publisher = {Springer-Verlag},

1594

  isbn = {3-540-78162-5, 978-3-540-78162-2},

1595

  location = {San Francisco, USA}

1596

1597

1598

@INPROCEEDINGS{Bouissou2008a,

1599

  author = {Bouissou, Olivier and Martel, Matthieu},

1600

  title = {A hybrid denotational semantics for hybrid systems},

1601

  booktitle = {ESOP'08/ETAPS'08: Proceedings of the Theory and practice of software,

1602

	17th European conference on Programming languages and systems},

1603

  year = {2008},

1604

  pages = {63--77},

1605

  address = {Berlin, Heidelberg},

1606

  publisher = {Springer-Verlag},

1607

  isbn = {3-540-78738-0, 978-3-540-78738-9},

1608

  location = {Budapest, Hungary}

1609

1610

1611

@ARTICLE{Bourque2004,

1612

  author = {Bourque, P. and Dupuis, R.},

1613

  title = {Guide to the Software Engineering Body of Knowledge 2004 Version},

1614

  journal = {Guide to the Software Engineering Body of Knowledge, 2004. SWEBOK},

1615

  year = {2004},

1616

  month = { }

1617

1618

1619

@MANUAL{Bouwer2005,

1620

  title = {User Manual for Single-User Version of QR Workbench},

1621

  author = {Bouwer, A. and Liem, J. and Bredeweg, B.},

1622

  organization = {Naturnet-Redime, STREP project co-funded by the European Commission

1623

	within the Sixth Framework Programme (2002-2006)},

1624

  year = {2005},

1625

  note = {Project no. 004074. Project deliverable D4.2.1.},

1626

  owner = {harald},

1627

  timestamp = {2009.09.18}

1628

1629

1630

@INPROCEEDINGS{Boyapati2002,

1631

  author = {Boyapati, Chandrasekhar and Khurshid, Sarfraz and Marinov, Darko

1632

},

1633

  title = {Korat: automated testing based on Java predicates},

1634

  booktitle = {ISSTA '02: Proceedings of the 2002 ACM SIGSOFT international symposium

1635

	on Software testing and analysis},

1636

  year = {2002},

1637

  pages = {123--133},

1638

  address = {New York, NY, USA},

1639

  publisher = {ACM},

1640

  abstract = {This paper presents Korat, a novel framework for automated testing

1641

	of Java programs. Given a formal specification for a method, Korat

1642

	uses the method precondition to automatically generate all (nonisomorphic)

1643

	test cases up to a given small size. Korat then executes the method

1644

	on each test case, and uses the method postcondition as a test oracle

1645

	to check the correctness of each output. To generate test cases for

1646

	a method, Korat constructs a Java predicate (i.e., a method that

1647

	returns a boolean) from the method's precondition. The heart of Korat

1648

	is a technique for automatic test case generation: given a predicate

1649

	and a bound on the size of its inputs, Korat generates all (nonisomorphic)

1650

	inputs for which the predicate returns true. Korat exhaustively explores

1651

	the bounded input space of the predicate but does so efficiently

1652

	by monitoring the predicate's executions and pruning large portions

1653

	of the search space. This paper illustrates the use of Korat for

1654

	testing several data structures, including some from the Java Collections

1655

	Framework. The experimental results show that it is feasible to generate

1656

	test cases from Java predicates, even when the search space for inputs

1657

	is very large. This paper also compares Korat with a testing framework

1658

	based on declarative specifications. Contrary to our initial expectation,

1659

	the experiments show that Korat generates test cases much faster

1660

	than the declarative framework.},

1661

  citeulike-article-id = {2638005},

1662

  doi = {http://doi.acm.org/10.1145/566172.566191},

1663

  keywords = {bibtex-import, boundingsymbolic, execution, loop},

1664

  local-url = {file://localhost/Users/michele/mogentes/bibliography/p123-boyapati.pdf},

1665

  owner = {harald},

1666

  posted-at = {2008-04-07 16:23:44},

1667

  priority = {2},

1668

  timestamp = {2009.09.18},

1669

  url = {http://dx.doi.org/10.1145/566172.566191}

1670

1671

1672

@INCOLLECTION{Bozga1998,

1673

  author = {Bozga, Marius and Daws, Conrado and Maler, Oded and Olivero, Alfredo

1674

	and Tripakis, Stavros and Yovine, Sergio},

1675

  title = {Kronos: A model-checking tool for real-time systems},

1676

  booktitle = {Formal Techniques in Real-Time and Fault-Tolerant Systems},

1677

  publisher = {Springer Berlin / Heidelberg},

1678

  year = {1998},

1679

  editor = {Ravn, Anders and Rischel, Hans},

1680

  volume = {1486},

1681

  series = {Lecture Notes in Computer Science},

1682

  pages = {298-302},

1683

  note = {10.1007/BFb0055357},

1684

  affiliation = {Verimag, Centre équation 2 avenue de Vignate 38610 Gières France 2

1685

	avenue de Vignate 38610 Gières France},

1686

  url = {http://dx.doi.org/10.1007/BFb0055357}

1687

1688

1689

@INPROCEEDINGS{Brandl2009,

1690

  author = {Harald Brandl},

1691

  title = {Testing of Hybrid Systems using Qualitative Models},

1692

  year = {2009},

1693

  editor = {MohammadReza Mousavi and Emil Sekerinski},

1694

  volume = {Proceedings of Formal Methods 2009 Doctoral Symposium},

1695

  pages = {46--52},

1696

  month = {11},

1697

  owner = {harald},

1698

  timestamp = {2010.10.09},

1699

  url = {http://www.win.tue.nl/~mousavi/fm09ds.pdf}

1700

1701

1702

@INPROCEEDINGS{Brandl2008,

1703

  author = {Harald Brandl and Gordon Fraser and Franz Wotawa},

1704

  title = {A report on {QR}-based testing},

1705

  booktitle = {22nd International Workshop on Qualitative Reasoning},

1706

  year = {2008},

1707

  pages = {1--9},

1708

  location = {Boulder, CO},

1709

  url = {www.cs.colorado.edu/~lizb/qr08/papers/Brandl.pdf}

1710

1711

1712

@INPROCEEDINGS{Brandl2008b,

1713

  author = {Harald Brandl and Gordon Fraser and Franz Wotawa},

1714

  title = {{QR}-model based testing},

1715

  booktitle = {AST '08: Proceedings of the 3rd international workshop on Automation

1716

	of software test},

1717

  year = {2008},

1718

  pages = {17--20},

1719

  address = {New York, NY, USA},

1720

  publisher = {ACM},

1721

  doi = {http://doi.acm.org/10.1145/1370042.1370046},

1722

  isbn = {978-1-60558-030-2},

1723

  location = {Leipzig, Germany},

1724

  owner = {harald},

1725

  timestamp = {2009.09.18}

1726

1727

1728

@ARTICLE{Brandl2010,

1729

  author = {Harald Brandl and Martin Weiglhofer and Bernhard K. Aichernig},

1730

  title = {Automated Conformance Verification of Hybrid Systems},

1731

  journal = {Quality Software, International Conference on},

1732

  year = {2010},

1733

  volume = {0},

1734

  pages = {3-12},

1735

  address = {Los Alamitos, CA, USA},

1736

  doi = {http://doi.ieeecomputersociety.org/10.1109/QSIC.2010.53},

1737

  issn = {1550-6002},

1738

  publisher = {IEEE Computer Society}

1739

1740

1741

@INPROCEEDINGS{Brandl2008a,

1742

  author = {Harald Brandl and Franz Wotawa},

1743

  title = {Test Case Generation from {QR} Models},

1744

  booktitle = {21st International Conference on Industrial, Engineering \& Other

1745

	Applications of Applied Intelligent Systems},

1746

  year = {2008},

1747

  owner = {harald},

1748

  timestamp = {2009.09.18}

1749

1750

1751

@ARTICLE{Braspenning2006,

1752

  author = {N. C. W. M. Braspenning and J. M. van de Mortel-Fronczak and J. E.

1753

	Rooda},

1754

  title = {A Model-based Integration and Testing Method to Reduce System Development

1755

	Effort},

1756

  journal = {Electr. Notes Theor. Comput. Sci.},

1757

  year = {2006},

1758

  volume = {164},

1759

  pages = {13-28},

1760

  number = {4},

1761

  bibsource = {DBLP, http://dblp.uni-trier.de},

1762

  ee = {http://dx.doi.org/10.1016/j.entcs.2006.09.003},

1763

  owner = {harald},

1764

  timestamp = {2009.09.18}

1765

1766

1767

@INPROCEEDINGS{Bredeweg2006,

1768

  author = {Bert Bredeweg and Anders Bouwer and Jelmer Jellema and Dirk Bertels

1769

	and Floris Floris Linnebank and Jochem Liem},

1770

  title = {Garp3 - A new Workbench for Qualitative Reasoning and Modelling},

1771

  booktitle = {Proceedings of 20th International Workshop on Qualitative Reasoning

1772

	(QR-06)},

1773

  year = {2006},

1774

  pages = {21-28},

1775

  address = {Hannover, New Hampshire, USA},

1776

  owner = {harald},

1777

  timestamp = {2009.09.18}

1778

1779

1780

@MANUAL{Bredeweg2005,

1781

  title = {Curriculum for learning about QR modelling},

1782

  author = {Bredeweg, B. and Liem, J. and Bouwer, A. and Salles, P},

1783

  organization = {Naturnet-Redime, STREP project co-funded by the European Commission

1784

	within the Sixth Framework Programme (2002-2006)},

1785

  year = {2005},

1786

  note = {Project no. 004074. Project deliverable D6.9.1.},

1787

  owner = {harald},

1788

  timestamp = {2009.09.18}

1789

1790

1791

@INPROCEEDINGS{Brinksma1988,

1792

  author = {Ed Brinksma},

1793

  title = {A theory for the derivation of tests},

1794

  booktitle = {Protocol Specification, Testing, and Verification VIII},

1795

  year = {1988},

1796

  editor = {S. Aggarwal and K. Sabnani},

1797

  pages = {402--416},

1798

  publisher = {North-Holland}

1799

1800

1801

@INPROCEEDINGS{Brinksma1995,

1802

  author = {Brinksma, Ed and Scollo, Giuseppe and Steenbergen, Chris},

1803

  title = {Lotos specifications, their implementations and their tests},

1804

  booktitle = {Conformance testing methodologies and architectures for OSI protocols},

1805

  year = {1995},

1806

  editor = {Richard Jerry Linn and M. {\"U}mit Uyar},

1807

  pages = {468--479},

1808

  address = {Los Alamitos, CA, USA},

1809

  publisher = {IEEE Computer Society Press},

1810

  isbn = {0-8186-5352-3}

1811

1812

1813

@INPROCEEDINGS{Brinksma2000,

1814

  author = {Ed Brinksma and Jan Tretmans},

1815

  title = {Testing Transition Systems: An Annotated Bibliography},

1816

  booktitle = {MOVEP},

1817

  year = {2000},

1818

  pages = {187-195},

1819

  bibsource = {DBLP, http://dblp.uni-trier.de},

1820

  ee = {http://link.springer.de/link/service/series/0558/bibs/2067/20670187.htm},

1821

  owner = {harald},

1822

  timestamp = {2009.09.18}

1823

1824

1825

@ARTICLE{Broy1999,

1826

  author = {Manfred Broy and Franz Huber and Bernhard Sch{\"a}tz},

1827

  title = {AutoFocus - Ein Werkzeugprototyp zur Entwicklung eingebetteter Systeme},

1828

  journal = {Inform., Forsch. Entwickl.},

1829

  year = {1999},

1830

  volume = {14},

1831

  pages = {121-134},

1832

  number = {3},

1833

  bibsource = {DBLP, http://dblp.uni-trier.de},

1834

  ee = {http://link.springer.de/link/service/journals/00450/bibs/9014003/90140121.htm},

1835

  owner = {harald},

1836

  timestamp = {2009.09.18}

1837

1838

1839

@INPROCEEDINGS{Brucker2008,

1840

  author = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},

1841

  title = {Verifying Test-Hypotheses -- An Experiment in Test and Proof},

1842

  booktitle = {Model-based Testing (MBT 2008)},

1843

  year = {2008},

1844

  editor = {Bernd Finkbeiner and Yuri Gurevich and Alexander K. Petrenko},

1845

  series = j-entcs,

1846

  address = {Budapest, Hungary},

1847

  publisher = {Elsevier Science Publishers},

1848

  note = {To appear.},

1849

  abstract = {\testgen is a specification and test case generation environment extending

1850

	the interactive theorem prover Isabelle/\acs{hol}. The \testgen method

1851

	is two-staged: first, the original formula, called \emph{test specification},

1852

	is partitioned into \emph{test cases} by transformation into a normal

1853

	form called \emph{test theorem}. Second, the test cases are analyzed

1854

	for ground instances (the \emph{test data}) satisfying the constraints

1855

	of the test cases. Particular emphasis is put on the control of explicit

1856

	test hypotheses which can be proven over concrete programs. As such,

1857

	explicit test hypotheses establish a logical link between validation

1858

	by test and by proof. Since \testgen generates explicit test hypotheses

1859

	and makes them amenable to formal proof, the system is in a unique

1860

	position to explore the relations between them at an example.},

1861

  categories = {holtestgen},

1862

  classification = {workshop},

1863

  file = {brucker.ea-verifying-2008.pdf:http\://www.brucker.ch/bibliography/download/2008/brucker.ea-verifying-2008.pdf:PDF;brucker.ea-verifying-2008.ps.gz:http\://www.brucker.ch/bibliography/download/2008/brucker.ea-verifying-2008.ps.gz:PostScript},

1864

  keywords = {symbolic test case generations, black box testing, theorem proving,

1865

	formal verification, Isabelle/HOL},

1866

  language = {USenglish},

1867

  owner = {harald},

1868

  public = {yes},

1869

  timestamp = {2009.09.18},

1870

  url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-verifying-2008}

1871

1872

1873

@ARTICLE{Bryant1986,

1874

  author = {Randal E. Bryant},

1875

  title = {Graph-based algorithms for Boolean function manipulation},

1876

  journal = {IEEE Trans. Comput.},

1877

  year = {1986},

1878

  volume = {35},

1879

  pages = {677--691},

1880

  number = {8},

1881

  address = {Washington, DC, USA},

1882

  issn = {0018-9340},

1883

  owner = {harald},

1884

  publisher = {IEEE Computer Society},

1885

  timestamp = {2009.09.18}

1886

1887

1888

@ARTICLE{Budd1985,

1889

  author = {Timothy Alan Budd and Ajei Sarat Gopal},

1890

  title = {Program Testing by Specification Mutation},

1891

  journal = {Computer Languages},

1892

  year = {1985},

1893

  volume = {10},

1894

  pages = {63-73},

1895

  owner = {wkrenn},

1896

  timestamp = {2009.09.17}

1897

1898

1899

@ARTICLE{Burdy2005,

1900

  author = {Lilian Burdy and Yoonsik Cheon and David R. Cok and Michael D. Ernst

1901

	and Joseph R. Kiniry and Gary T. Leavens and K. Rustan M. Leino and

1902

	Erik Poll},

1903

  title = {An overview of JML tools and applications},

1904

  journal = {STTT},

1905

  year = {2005},

1906

  volume = {7},

1907

  pages = {212-232},

1908

  number = {3},

1909

  bibsource = {DBLP, http://dblp.uni-trier.de},

1910

  ee = {http://dx.doi.org/10.1007/s10009-004-0167-4},

1911

  owner = {harald},

1912

  timestamp = {2009.09.18}

1913

1914

1915

@INPROCEEDINGS{Callahan1996,

1916

  author = {John Callahan and Francis Schneider and Steve Easterbrook},

1917

  title = {Automated {S}oftware {T}esting {U}sing {M}odel-{C}hecking},

1918

  booktitle = {Proceedings 1996 {SPIN} {W}orkshop},

1919

  year = {1996},

1920

  month = {August},

1921

  note = {Also WVU Technical Report NASA-IVV-96-022.},

1922

  owner = {gordon},

1923

  timestamp = {2009.09.18}

1924

1925

1926

@TECHREPORT{Campbell,

1927

  author = {Campbell, Colin and Grieskamp, Wolfgang and Nachmanson, Lev and Schulte,

1928

	Wolfram and Tillmann, Nikolai and Veanes, Margus },

1929

  title = {Model-Based Testing of Object-Oriented Reactive Systems with Spec

1930

	Explorer},

1931

  abstract = {Testing is one of the costliest aspects of commercial software development.

1932

	Model-based testing is a promising approach addressing these deficits.

1933

	At Microsoft, model-based testing technology developed by the Foundations

1934

	of Software Engineering group in Microsoft Research has been used

1935

	since 2003. The second generation of this tool set, Spec Explorer,

1936

	deployed in 2004, is now used on a daily basis by Microsoft product

1937

	groups for testing operating system components, .NET framework components

1938

	and other areas. This paper provides a comprehensive survey of the

1939

	concepts of the tool and their foundations.},

1940

  citeulike-article-id = {2626080},

1941

  keywords = {microsoft, spec, testing},

1942

  owner = {harald},

1943

  posted-at = {2008-04-07 15:41:30},

1944

  priority = {0},

1945

  school = {Microsoft Research},

1946

  timestamp = {2009.09.18},

1947

  url = {ftp://ftp.research.microsoft.com/pub/tr/TR-2005-59.pdf}

1948

1949

1950

@INPROCEEDINGS{Cavalcanti2007,

1951

  author = {Cavalcanti, Ana and Gaudel, Marie-Claude},

1952

  title = {Testing for refinement in CSP},

1953

  booktitle = {ICFEM'07: Proceedings of the formal engineering methods 9th international

1954

	conference on Formal methods and software engineering},

1955

  year = {2007},

1956

  pages = {151--170},

1957

  address = {Berlin, Heidelberg},

1958

  publisher = {Springer-Verlag},

1959

  isbn = {3-540-76648-0, 978-3-540-76648-3},

1960

  location = {Boca Raton, FL, USA}

1961

1962

1963

@UNPUBLISHED{Cengarle,

1964

  author = {Maria Victoria Cengarle and Armando Martin Haeberer},

1965

  title = {Towards an epistemology-based methodology for verification and validation

1966

	testing},

1967

  note = {Technical report, Ludwig-Maximilians-Universit\"at M\"{u}nchen, unpublished

1968

	draft of March 2, 2000},

1969

  libnum = {195},

1970

  owner = {harald},

1971

  timestamp = {2009.09.18}

1972

1973

1974

@INPROCEEDINGS{Cengarle2000,

1975

  author = {Maria Victoria Cengarle and Armando Martin Haeberer},

1976

  title = {{A formal approach to specification-based black-box testing}},

1977

  booktitle = {{Proceedings of the Workshop on Modelling Software System Structures

1978

	in a Fastly Moving Scenario, June 13-16, 2000, Santa Margherita Ligure,

1979

	Italia}},

1980

  year = {2000},

1981

  libnum = {196},

1982

  owner = {harald},

1983

  timestamp = {2009.09.18}

1984

1985

1986

@ARTICLE{Chen2001,

1987

  author = {H.Y. Chen and T.H. Tse and T.Y. Chen},

1988

  title = {{TACCLE}: a methodology for object-oriented software testing at the

1989

	class and cluster levels},

1990

  journal = {ACM Transactions on Software Engineering and Methodology},

1991

  year = {2001},

1992

  volume = {10},

1993

  pages = {56--109},

1994

  number = {1},

1995

  owner = {harald},

1996

  timestamp = {2009.09.18}

1997

1998

1999

@INPROCEEDINGS{Cheng1993,

2000

  author = {Kwang-Ting Cheng and A. S. Krishnakumar},

2001

  title = {Automatic Functional Test Generation Using the Extended Finite State

2002

	Machine Model},

2003

  booktitle = {DAC},

2004

  year = {1993},

2005

  pages = {86-91},

2006

  bibsource = {DBLP, http://dblp.uni-trier.de},

2007

  ee = {http://doi.acm.org/10.1145/157485.164585},

2008

  owner = {harald},

2009

  timestamp = {2009.09.18}

2010

2011

2012

@INPROCEEDINGS{Cheon2008,

2013

  author = {Yoonsik Cheon and Antonio Cortes and Martine Ceberio and Gary T.

2014

	Leavens},

2015

  title = {Integrating Random Testing with Constraints for Improved Efficiency

2016

	and Diversity},

2017

  booktitle = {Proceedings of the International Conference on Software Engineering

2018

	and Knowledge Engineering},

2019

  year = {2008},

2020

  month = {February},

2021

  organization = {Department of Computer Science, The University of Texas at El Paso},

2022

  note = {to appear},

2023

  owner = {harald},

2024

  timestamp = {2009.09.18}

2025

2026

2027

@INPROCEEDINGS{Cimatti1999,

2028

  author = {Alessandro Cimatti and Edmund M. Clarke and Fausto Giunchiglia and

2029

	Marco Roveri},

2030

  title = {N{USMV}: {A} {N}ew {S}ymbolic {M}odel {V}erifier},

2031

  booktitle = {C{AV} '99: {P}roceedings of the 11th {I}nternational {C}onference

2032

	on {C}omputer {A}ided {V}erification},

2033

  year = {1999},

2034

  pages = {495--499},

2035

  address = {London, UK},

2036

  publisher = {Springer-Verlag},

2037

  isbn = {3-540-66202-2},

2038

  owner = {harald},

2039

  timestamp = {2009.09.18}

2040

2041

2042

@ARTICLE{Claessen2002,

2043

  author = {Koen Claessen and John Hughes},

2044

  title = {Testing monadic code with QuickCheck},

2045

  journal = {SIGPLAN Notices},

2046

  year = {2002},

2047

  volume = {37},

2048

  pages = {47-59},

2049

  number = {12},

2050

  bibsource = {DBLP, http://dblp.uni-trier.de},

2051

  ee = {http://doi.acm.org/10.1145/636517.636527},

2052

  owner = {harald},

2053

  timestamp = {2009.09.18}

2054

2055

2056

@INPROCEEDINGS{Claessen2000,

2057

  author = {Koen Claessen and John Hughes},

2058

  title = {QuickCheck: a lightweight tool for random testing of Haskell programs},

2059

  booktitle = {ICFP},

2060

  year = {2000},

2061

  pages = {268-279},

2062

  bibsource = {DBLP, http://dblp.uni-trier.de},

2063

  ee = {http://doi.acm.org/10.1145/351240.351266},

2064

  owner = {harald},

2065

  timestamp = {2009.09.18}

2066

2067

2068

@INPROCEEDINGS{Claessen2000a,

2069

  author = {K. Claessen and J. Hughes},

2070

  title = {{Quickcheck}: a lightweight tool for random testing of {Haskell}

2071

	programs},

2072

  booktitle = {Fifth ACM SIGPLAN International Conference on Functional Programming},

2073

  year = {2000},

2074

  pages = {268--279},

2075

  publisher = {ACM Press},

2076

  owner = {harald},

2077

  timestamp = {2009.09.18}

2078

2079

2080

@INPROCEEDINGS{Clarke2000,

2081

  author = {Clarke, Edmund and Grumberg, Orna and Jha, Somesh and Lu, Yuan and

2082

	Veith, Helmut},

2083

  title = {Counterexample-Guided Abstraction Refinement},

2084

  booktitle = {Computer Aided Verification, 12th International Conference},

2085

  year = {2000},

2086

  pages = {154--169},

2087

  journal = {Computer Aided Verification},

2088

  owner = {wkrenn},

2089

  timestamp = {2009.09.18},

2090

  url = {http://dx.doi.org/10.1007/10722167_15}

2091

2092

2093

@INPROCEEDINGS{Clarke2004,

2094

  author = { Clarke, Edmund and Kroening, Daniel and Lerda, Flavio },

2095

  title = { A Tool for Checking {ANSI-C} Programs },

2096

  booktitle = { Tools and Algorithms for the Construction and Analysis of Systems

2097

	(TACAS 2004) },

2098

  year = { 2004 },

2099

  editor = { Kurt Jensen and Andreas Podelski },

2100

  volume = { 2988 },

2101

  series = { Lecture Notes in Computer Science },

2102

  pages = { 168--176 },

2103

  publisher = { Springer },

2104

  isbn = { 3-540-21299-X },

2105

  owner = {harald},

2106

  timestamp = {2009.09.18}

2107

2108

2109

@INPROCEEDINGS{Clarke1982,

2110

  author = {Edmund M. Clarke and E. Allen Emerson},

2111

  title = {Design and Synthesis of Synchronization Skeletons Using Branching-Time

2112

	Temporal Logic},

2113

  booktitle = {Logic of Programs, Workshop},

2114

  year = {1982},

2115

  pages = {52--71},

2116

  address = {London, UK},

2117

  publisher = {Springer-Verlag},

2118

  isbn = {3-540-11212-X},

2119

  owner = {harald},

2120

  timestamp = {2009.09.18}

2121

2122

2123

@ARTICLE{Clarke1976,

2124

  author = {Clarke, L. A. },

2125

  title = {A System to Generate Test Data and Symbolically Execute Programs},

2126

  journal = {IEEE Transactions on Software Engineering},

2127

  year = {1976},

2128

  volume = {2},

2129

  pages = {215--222},

2130

  number = {3},

2131

  abstract = {This paper describes a system that attempts to generate test data

2132

	for programs written in ANSI Fortran. Given a path, the system symbolically

2133

	executes the path and creates a set of constraints on the program's

2134

	input variables. If the set of constraints is linear, linear pro-

2135

	gramming techniques are employed to obtain a solution. A solution

2136

	to the set of constraints is test data that will drive execution

2137

	down the given path. If it can be determined that the set of constraints

2138

	is incon- sistent, then the given path is shown to be nonexecutable.

2139

	To increase the chance of detecting some of the more common programming

2140

	errors, artificial constraints are temporarily created that simulate

2141

	error condi- tions and then an attempt is made to solve each augmented

2142

	set of constraints. A symbolic representation of the program's output

2143

	vari- ables in terms of the program's input variables is also created.

2144

	The symbolic representation is in a human readable form that facilitates

2145

	error detection as weUl as being a possible aid in assertion generation

2146

	and automatic program documentation.},

2147

  address = {Los Alamitos, CA, USA},

2148

  citeulike-article-id = {2638013},

2149

  doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.1976.233817},

2150

  keywords = {bibtex-import, execution, generationsymbolic, test, vector},

2151

  local-url = {file://localhost/Users/michele/mogentes/bibliography/01702368.pdf},

2152

  owner = {harald},

2153

  posted-at = {2008-04-07 16:23:45},

2154

  priority = {2},

2155

  publisher = {IEEE Computer Society},

2156

  timestamp = {2009.09.18},

2157

  url = {http://dx.doi.org/http://doi.ieeecomputersociety.org/10.1109/TSE.1976.233817}

2158

2159

2160

@ARTICLE{Clarke1989,

2161

  author = {L. A. Clarke and A. Podgurski and D. J. Richardson and S. J. Zeil},

2162

  title = {A Formal Evaluation of Data Flow Path Selection Criteria},

2163

  journal = {IEEE Trans. Softw. Eng.},

2164

  year = {1989},

2165

  volume = {15},

2166

  pages = {1318--1332},

2167

  number = {11},

2168

  address = {Piscataway, NJ, USA},

2169

  doi = {http://dx.doi.org/10.1109/32.41326},

2170

  issn = {0098-5589},

2171

  owner = {harald},

2172

  publisher = {IEEE Press},

2173

  timestamp = {2009.09.18}

2174

2175

2176

@INPROCEEDINGS{Cleaveland1991,

2177

  author = {R. Cleaveland and A. E. Zwarico},

2178

  title = {A Theory of Testing for Real-Time},

2179

  booktitle = {Proc.\ of the Sixth Annual IEEE Symposium on Logic in Computer Science},

2180

  year = {1991},

2181

  pages = {110-119},

2182

  address = {Amsterdam, The Netherlands},

2183

  owner = {harald},

2184

  timestamp = {2009.09.18}

2185

2186

2187

@INPROCEEDINGS{Craggs2003,

2188

  author = {Ian Craggs and Manolis Sardis and Thierry Heuillard},

2189

  title = {AGEDIS Case Studies: Model-Based Testing in Industry},

2190

  booktitle = {Proceedings of the 1st European Conference on Model Driven Software

2191

	Engineering},

2192

  year = {2003},

2193

  pages = {106--117},

2194

  owner = {harald},

2195

  timestamp = {2009.09.18}

2196

2197

2198

@ARTICLE{D'Silva2008,

2199

  author = {D'Silva, Vijay and Kroening, Daniel and Weissenbacher, Georg },

2200

  title = {A Survey of Automated Techniques for Formal Software Verification},

2201

  journal = {A Survey of Automated Techniques for Formal Software Verification},

2202

  year = {2008},

2203

  abstract = {<p>The quality and the correctness of software is often the greatest

2204

	<br />concern in electronic systems. Formal verification tools can

2205

	provide a<br />guarantee that a design is free of specific flaws.

2206

	This paper surveys<br />algorithms that perform automatic, static

2207

	analysis of software to detect<br />programming errors or prove their

2208

	absence. The three techniques considered<br />are static analysis

2209

	with abstract domains, model checking, and bounded model<br />checking.

2210

	A short tutorial on these techniques is provided, highlighting<br

2211

	/>their differences when applied to practical problems. The paper

2212

	also surveys<br />the tools that are available implementing these

2213

	techniques, and describes<br />their merits and shortcomings.</p>},

2214

  citeulike-article-id = {2762806},

2215

  keywords = {mogentes},

2216

  owner = {harald},

2217

  posted-at = {2008-05-06 21:09:47},

2218

  priority = {2},

2219

  publisher = {IEEE},

2220

  timestamp = {2009.09.18},

2221

  url = {http://www.kroening.com/publications/view-publications-dkw2008.html}

2222

2223

2224

@INPROCEEDINGS{Dan2004,

2225

  author = {Li Dan and Bernhard K. Aichernig},

2226

  title = {Combining Algebraic and Model-based Test Case Generation},

2227

  booktitle = {Proceedings of First International Colloquium on Theoretical Aspects

2228

	of Computing, Guiyang, China 20-24 September 2004},

2229

  year = {2004},

2230

  volume = {3407},

2231

  series = {Lecture Notes in Computer Science},

2232

  pages = {250--264},

2233

  publisher = {Springer-Verlag},

2234

  owner = {harald},

2235

  timestamp = {2009.09.18}

2236

2237

2238

@INPROCEEDINGS{Dang2008,

2239

  author = {Dang, Thao and Nahhal, Tarik},

2240

  title = {Using Disparity to Enhance Test Generation for Hybrid Systems},

2241

  booktitle = {TestCom '08 / FATES '08: Proceedings of the 20th IFIP TC 6/WG 6.1

2242

	international conference on Testing of Software and Communicating

2243

	Systems},

2244

  year = {2008},

2245

  pages = {54--69},

2246

  address = {Berlin, Heidelberg},

2247

  publisher = {Springer-Verlag},

2248

  doi = {http://dx.doi.org/10.1007/978-3-540-68524-1_6},

2249

  isbn = {978-3-540-68514-2},

2250

  location = {Tokyo, Japan}

2251

2252

2253

@ARTICLE{Dauchy1993,

2254

  author = {Pierre Dauchy and Marie-Claude Gaudel and Bruno Marre},

2255

  title = {Using algebraic specifications in software testing: A case study

2256

	on the software of an automatic subway},

2257

  journal = {Journal of Systems and Software},

2258

  year = {1993},

2259

  volume = {21},

2260

  pages = {229-244},

2261

  number = {3},

2262

  bibsource = {DBLP, http://dblp.uni-trier.de},

2263

  ee = {http://dx.doi.org/10.1016/0164-1212(93)90025-S},

2264

  owner = {harald},

2265

  timestamp = {2009.09.18}

2266

2267

2268

@INPROCEEDINGS{Daws1995,

2269

  author = {Conrado Daws and Alfredo Olivero and Sergio Yovine},

2270

  title = {Verifying ET-LOTOS programmes with KRONOS},

2271

  booktitle = {Proceedings of the 7th IFIP WG6.1 International Conference on Formal

2272

	Description Techniques VII},

2273

  year = {1995},

2274

  pages = {227--242},

2275

  address = {London, UK, UK},

2276

  publisher = {Chapman \& Hall, Ltd.},

2277

  isbn = {0-412-64450-9},

2278

  owner = {harald},

2279

  timestamp = {2009.09.18}

2280

2281

2282

@ARTICLE{DeJong2004,

2283

  author = {De Jong, Hidde},

2284

  title = {Qualitative simulation and related approaches for the analysis of

2285

	dynamic systems},

2286

  journal = {Knowl. Eng. Rev.},

2287

  year = {2004},

2288

  volume = {19},

2289

  pages = {93--132},

2290

  number = {2},

2291

  address = {New York, NY, USA},

2292

  doi = {http://dx.doi.org/10.1017/S0269888904000177},

2293

  issn = {0269-8889},

2294

  publisher = {Cambridge University Press}

2295

2296

2297

@ARTICLE{DeMillo1978,

2298

  author = {Richard A. DeMillo and Richard J. Lipton and Frederick G. Sayward},

2299

  title = {Hints on {T}est {D}ata {S}election: {H}elp for the {P}racticing {P}rogrammer},

2300

  journal = {Computer},

2301

  year = {1978},

2302

  volume = {11},

2303

  pages = {34-41},

2304

  owner = {gordon},

2305

  timestamp = {2009.09.18}

2306

2307

2308

@INPROCEEDINGS{Derksen2007,

2309

  author = {Derksen, Roger and van der Wouden, Huub and Heath, Paul},

2310

  title = {Testing The Heathrow Terminal 5 Baggage Handling System - Before

2311

	It Is Built},

2312

  year = {2007},

2313

  month = {November},

2314

  abstract = {London Heathrow Terminal 5 will open in March 2008. This new core

2315

	terminal building and two satellites will handle 30 million passengers

2316

	a year, and all of these passengers will expect their baggage to

2317

	accompany them on their flights. To achieve this, a new baggage handling

2318

	system is being constructed that will handle more than 70,000 bags

2319

	a day. Maintaining customer confidence in the reliability of the

2320

	baggage handling system is vital to the successful delivery of the

2321

	project. The challenge for the baggage control system designers was

2322

	how best to integrate and test the software systems of such a large

2323

	and complex system within a limited time to test the software in

2324

	its actual site environment. This article explains the vital role

2325

	that software emulation testing techniques played in factory integration

2326

	testing. The advantages and limitations of these techniques are covered

2327

	along with explanations of what can (and cannot) be achieved in the

2328

	factory environment.},

2329

  citeulike-article-id = {2802474},

2330

  keywords = {mogentes, testing},

2331

  owner = {harald},

2332

  posted-at = {2008-05-15 19:54:12},

2333

  priority = {3},

2334

  timestamp = {2009.09.18}

2335

2336

2337

@BOOK{DeRoever1999,

2338

  title = {Data Refinement: Model-Oriented Proof Methods and Their Comparison},

2339

  publisher = {Cambridge University Press},

2340

  year = {1999},

2341

  author = {DeRoever,, W. and Engelhardt,, Kai},

2342

  address = {New York, NY, USA},

2343

  isbn = {0521641705},

2344

  owner = {harald},

2345

  timestamp = {2009.09.18}

2346

2347

2348

@INPROCEEDINGS{Dick1993a,

2349

  author = {Jeremy Dick and Alain Faivre},

2350

  title = {Automating the Generation and Sequencing of Test Cases from Model-Based

2351

	Specifications},

2352

  booktitle = {Proceedings of FME'93: Industrial-Strength Formal Methods, International

2353

	Symposium of Formal Methods Europe, April 1993, Odense, Denmark},

2354

  year = {1993},

2355

  editor = {J.C.P. Woodcock and P.G. Larsen},

2356

  pages = {268--284},

2357

  month = {April},

2358

  publisher = {Springer-Verlag},

2359

  libnum = {7},

2360

  owner = {harald},

2361

  timestamp = {2009.09.18}

2362

2363

2364

@INPROCEEDINGS{Dick1993,

2365

  author = {Dick, Jeremy and Faivre, Alain },

2366

  title = {Automating the Generation and Sequencing of Test Cases from Model-Based

2367

	Specifications},

2368

  booktitle = {FME '93: Proceedings of the First International Symposium of Formal

2369

	Methods Europe on Industrial-Strength Formal Methods},

2370

  year = {1993},

2371

  pages = {268--284},

2372

  address = {London, UK},

2373

  publisher = {Springer-Verlag},

2374

  citeulike-article-id = {2649305},

2375

  isbn = {3540566627},

2376

  keywords = {model, mogentes, testing},

2377

  owner = {harald},

2378

  posted-at = {2008-04-10 14:43:12},

2379

  priority = {2},

2380

  timestamp = {2009.09.18},

2381

  url = {http://portal.acm.org/citation.cfm?id=647535.729387}

2382

2383

2384

@BOOK{Dijkstra1990,

2385

  title = {Predicate Calculus and Program Semantics},

2386

  publisher = {Springer-Verlag},

2387

  year = {1990},

2388

  author = {E.W. Dijkstra and C.S. Scholten},

2389

  series = {Texts and Monographs in Computer Science},

2390

  owner = {harald},

2391

  timestamp = {2009.09.18}

2392

2393

2394

@INPROCEEDINGS{Dill1990,

2395

  author = {D. L. Dill},

2396

  title = {Timing assumptions and verification of finite-state concurrent systems},

2397

  booktitle = {Proceedings of the international workshop on Automatic verification

2398

	methods for finite state systems},

2399

  year = {1990},

2400

  pages = {197--212},

2401

  address = {New York, NY, USA},

2402

  publisher = {Springer-Verlag New York, Inc.},

2403

  isbn = {0-387-52148-8},

2404

  location = {Grenoble, France},

2405

  owner = {harald},

2406

  timestamp = {2009.09.18}

2407

2408

2409

@ARTICLE{Dong1994,

2410

  author = {R.K. Dong and Ph.G. Frankl},

2411

  title = {The {ASTOOT} approach to testing object-oriented programs},

2412

  journal = {ACM Transactions on Software Engineering and Methodology},

2413

  year = {1994},

2414

  volume = {3},

2415

  pages = {103--130},

2416

  number = {2},

2417

  owner = {harald},

2418

  timestamp = {2009.09.18}

2419

2420

2421

@ARTICLE{Dowson1997,

2422

  author = {Mark Dowson},

2423

  title = {{The ARIANE 5 Software Failure}},

2424

  journal = {{ACM SIGSOFT Software Engineering Notes}},

2425

  year = {1997},

2426

  volume = {22},

2427

  pages = {84},

2428

  number = {2},

2429

  address = {New York, NY, USA},

2430

  file = {:home/elisabeth/Diplomarbeit/Literatur/PDFs/ariane5.pdf:PDF},

2431

  issn = {0163-5948},

2432

  publisher = {ACM},

2433

  url = {http://portal.acm.org/citation.cfm?id=251992}

2434

2435

2436

@INPROCEEDINGS{Durrieu2004,

2437

  author = {Guy Durrieu and Odile Laurent and Christel Seguin and Virginie Wiels},

2438

  title = {Formal Proof and Test Case Generation for Critical Embedded Systems

2439

	Using Scade},

2440

  booktitle = {Building the Information Society, IFIP 18th World Computer Congress},

2441

  year = {2004},

2442

  editor = {Ren{\'e} Jacquart},

2443

  volume = {156/2004},

2444

  series = {IFIP International Federation for Information Processing},

2445

  pages = {499--504},

2446

  publisher = {Springer Boston},

2447

  doi = {10.1007/978-1-4020-8157-6_44},

2448

  owner = {harald},

2449

  timestamp = {2009.09.18}

2450

2451

2452

@MISC{Dutertre2006,

2453

  author = {Dutertre, B. and de Moura, L.},

2454

  title = {The Yices SMT solver},

2455

  howpublished = {Tool paper at http://yices.csl.sri.com/tool-paper.pdf},

2456

  month = {August},

2457

  year = {2006},

2458

  citeulike-article-id = {2639925},

2459

  keywords = {sat-solvers},

2460

  organization = {SRI International},

2461

  posted-at = {2008-04-08 04:25:43},

2462

  priority = {2}

2463

2464

2465

@INPROCEEDINGS{Emerson1982,

2466

  author = {E. Allen Emerson and Joseph Y. Halpern},

2467

  title = {Decision procedures and expressiveness in the temporal logic of branching

2468

	time},

2469

  booktitle = {STOC '82: Proceedings of the fourteenth annual ACM symposium on Theory

2470

	of computing},

2471

  year = {1982},

2472

  pages = {169--180},

2473

  address = {New York, NY, USA},

2474

  publisher = {ACM Press},

2475

  doi = {10.1145/800070.802190},

2476

  isbn = {0-89791-070-2},

2477

  location = {San Francisco, California, United States},

2478

  owner = {harald},

2479

  timestamp = {2009.09.18}

2480

2481

2482

@ARTICLE{Emerson1987,

2483

  author = {E. Allen Emerson and Chin-Laung Lei},

2484

  title = {Modalities for model checking: branching time logic strikes back},

2485

  journal = {Sci. Comput. Program.},

2486

  year = {1987},

2487

  volume = {8},

2488

  pages = {275--306},

2489

  number = {3},

2490

  address = {Amsterdam, The Netherlands, The Netherlands},

2491

  doi = {http://dx.doi.org/10.1016/0167-6423(87)90036-0},

2492

  issn = {0167-6423},

2493

  owner = {harald},

2494

  publisher = {Elsevier North-Holland, Inc.},

2495

  timestamp = {2009.09.18}

2496

2497

2498

@INPROCEEDINGS{Engels1997,

2499

  author = {Andr\'{e} Engels and Loe Feijs and Sjouke Mauw},

2500

  title = {Test Generation for Intelligent Networks Using ModelChecking},

2501

  booktitle = {Proceedings of the Third International Workshop on Tools and Algorithms

2502

	for the Construction and Analysis of Systems. (TACAS'97)},

2503

  year = {1997},

2504

  editor = {Ed Brinksma},

2505

  volume = {1217},

2506

  series = {Lecture Notes in Computer Science},

2507

  address = {Enschede, the Netherlands},

2508

  month = {April},

2509

  publisher = {Springer-Verlag},

2510

  optnote = {personal copy in Test 1},

2511

  owner = {harald},

2512

  timestamp = {2009.09.18}

2513

2514

2515

@ARTICLE{Esposito2004,

2516

  author = {Esposito, J.M.},

2517

  title = {Randomized test case generation for hybrid systems: metric selection},

2518

  journal = {System Theory, 2004. Proceedings of the Thirty-Sixth Southeastern

2519

	Symposium on System Theory},

2520

  year = {2004},

2521

  pages = {236-240},

2522

  doi = {10.1109/SSST.2004.1295655},

2523

  keywords = {computational complexity, control system analysis, path planning,

2524

	randomised algorithms, reachability analysis control systems, hybrid

2525

	state space, hybrid systems, metric selection, randomized approach,

2526

	robotic path planning, test case generation},

2527

  owner = {harald},

2528

  timestamp = {2009.09.18}

2529

2530

2531

@MISC{Farquhar1993,

2532

  author = {Adam Farquhar and Benjamin Kuipers and Jeff Rickel and David Throop

2533

	and The Qualitative Reasoning Group},

2534

  title = {{QSIM}: The Program and its Use},

2535

  month = {July},

2536

  year = {1993},

2537

  owner = {harald},

2538

  timestamp = {2010.08.11}

2539

2540

2541

@INPROCEEDINGS{Floyd1967,

2542

  author = {Robert W. Floyd},

2543

  title = {Assigning meanings to programs},

2544

  booktitle = {{P}roc. {A}mer. {M}ath. {S}oc. {S}ymposia in {A}pplied {M}athematics},

2545

  year = {1967},

2546

  volume = {19},

2547

  pages = {19--32},

2548

  publisher = {Amer. Math. Soc.},

2549

  owner = {harald},

2550

  timestamp = {2009.09.18},

2551

  url = {http://www.ams.org/mathscinet-getitem?mr=235771}

2552

2553

2554

@ARTICLE{Forbus1984,

2555

  author = {Kenneth D. Forbus},

2556

  title = {Qualitative Process Theory},

2557

  journal = {Artif. Intell.},

2558

  year = {1984},

2559

  volume = {24},

2560

  pages = {85-168},

2561

  number = {1-3},

2562

  bibsource = {DBLP, http://dblp.uni-trier.de}

2563

2564

2565

@INPROCEEDINGS{Foster2007,

2566

  author = {Howard Foster and Wolfgang Emmerich and Jeff Kramer and Jeff Magee

2567

	and David S. Rosenblum and Sebasti{\'a}n Uchitel},

2568

  title = {Model Checking Service Compositions under Resource Constraints},

2569

  booktitle = {Proceedings of the 6th joint meeting of the European Software Engineering

2570

	Conference and the ACM SIGSOFT International Symposium on Foundations

2571

	of Software Engineering ({ESEC/SIGSOFT FSE})},

2572

  year = {2007},

2573

  editor = {Ivica Crnkovic and Antonia Bertolino},

2574

  pages = {225--234},

2575

  publisher = {ACM},

2576

  owner = {harald},

2577

  timestamp = {2009.09.18}

2578

2579

2580

@INPROCEEDINGS{Frantzen2006,

2581

  author = {Lars Frantzen and Jan Tretmans and Tim A. C. Willemse},

2582

  title = {A Symbolic Framework for Model-Based Testing},

2583

  booktitle = {1st Combined International Workshops on Formal Approaches to Software

2584

	Testing and Runtime Verification},

2585

  year = {2006},

2586

  volume = {4262},

2587

  series = {LNCS},

2588

  pages = {40--54},

2589

  publisher = {Springer},

2590

  comment = {p,r},

2591

  ee = {http://dx.doi.org/10.1007/11940197_3},

2592

  file = {frantzen2006symbolic.pdf:frantzen2006symbolic.pdf:PDF},

2593

  owner = {martin},

2594

  timestamp = {2007.10.24}

2595

2596

2597

@ARTICLE{Fraser2007a,

2598

  author = {Fraser, Gordon and Aichernig, Bernhard K. and Wotawa, Franz },

2599

  title = {Handling Model Changes: Regression Testing and Test-Suite Update

2600

	with Model-Checkers},

2601

  journal = {Electronic Notes in Theoretical Computer Science},

2602

  year = {2007},

2603

  volume = {190},

2604

  pages = {33--46},

2605

  number = {2},

2606

  abstract = {Several model-checker based methods to automated test-case generation

2607

	have been proposed recently. The performance and applicability largely

2608

	depends on the complexity of the model in use. For complex models,

2609

	the costs of creating a full test-suite can be significant. If the

2610

	model is changed, then in general the test-suite is completely regenerated.

2611

	However, only a subset of a test-suite might be invalidated by a

2612

	model change. Creating a full test-suite in such a case would therefore

2613

	waste time by unnecessarily recreating valid test-cases. This paper

2614

	investigates methods to reduce the effort of recreating test-suites

2615

	after a model is changed. This is also related to regression testing,

2616

	where the number of test-cases necessary after a change should be

2617

	minimized. This paper presents and evaluates methods to identify

2618

	obsolete test-cases, and to extend any given test-case generation

2619

	approach based on model-checkers in order to create test-cases for

2620

	test-suite update or regression testing.},

2621

  citeulike-article-id = {2637990},

2622

  keywords = {automated, bibtex-import, change, generation, model, model-checkers,

2623

	regression, test-case, testing, test-suite, tug, update, with},

2624

  local-url = {file://localhost/Users/michele/mogentes/bibliography/mbt07.pdf},

2625

  owner = {harald},

2626

  posted-at = {2008-04-07 16:23:41},

2627

  priority = {2},

2628

  timestamp = {2009.09.18},

2629

  url = {http://www.sciencedirect.com/science/article/B75H1-4PHSRDB-4/2/320e4bc91ad12d87ea9ded2f18cc69f9}

2630

2631

2632

@INPROCEEDINGS{Fraser2008b,

2633

  author = {Gordon Fraser and Martin Weiglhofer and Franz Wotawa},

2634

  title = {Using Observer Automata to Select Test Cases for Test Purposes},

2635

  booktitle = {Proceedings of the 20th International Conference on Software Engineering

2636

	and Knowledge Engineering},

2637

  year = {2008},

2638

  note = {to appear},

2639

  comment = {a},

2640

  file = {fraser2008using.pdf:fraser2008using.pdf:PDF},

2641

  owner = {martin},

2642

  timestamp = {2008.05.20}

2643

2644

2645

@INPROCEEDINGS{Fraser2008c,

2646

  author = {Gordon Fraser and Martin Weiglhofer and Franz Wotawa},

2647

  title = {Coverage Based Testing with Test Purposes},

2648

  booktitle = {Proceedings of the 8th International Conference on Quality Software},

2649

  year = {2008},

2650

  note = {to appear},

2651

  comment = {a},

2652

  owner = {martin},

2653

  timestamp = {2008.05.20}

2654

2655

2656

@INPROCEEDINGS{Fraser2007,

2657

  author = {Fraser, Gordon and Wotawa, Franz},

2658

  title = {Test-Case Generation and Coverage Analysis for Nondeterministic Systems

2659

	Using Model-Checkers},

2660

  booktitle = {ICSEA '07: Proceedings of the International Conference on Software

2661

	Engineering Advances},

2662

  year = {2007},

2663

  pages = {45},

2664

  address = {Washington, DC, USA},

2665

  publisher = {IEEE Computer Society},

2666

  doi = {http://dx.doi.org/10.1109/ICSEA.2007.71},

2667

  isbn = {0-7695-2937-2},

2668

  owner = {harald},

2669

  timestamp = {2009.09.18}

2670

2671

2672

@ARTICLE{Fraser2008,

2673

  author = {Gordon Fraser and Franz Wotawa and Paul E. Ammann},

2674

  title = {Testing with model checkers: a survey},

2675

  journal = {Software Testing, Verification and Reliability},

2676

  year = {2008},

2677

  month = {December},

2678

  note = {accepted for publication},

2679

  doi = {10.1002/stvr.402},

2680

  owner = {martin},

2681

  timestamp = {2009.05.15}

2682

2683

2684

@INPROCEEDINGS{Friedman2002,

2685

  author = {G. Friedman and A. Hartman and K. Nagin and T. Shiran},

2686

  title = {Projected state machine coverage for software testing},

2687

  booktitle = {ISSTA},

2688

  year = {2002},

2689

  pages = {134-143},

2690

  bibsource = {DBLP, http://dblp.uni-trier.de},

2691

  ee = {http://doi.acm.org/10.1145/566172.566192},

2692

  owner = {harald},

2693

  timestamp = {2009.09.18}

2694

2695

2696

@INPROCEEDINGS{Futatsugi1995,

2697

  author = {K.~Futatsugi and J.A.~Goguen and J.P.~Jouannaud and J.~Meseguer},

2698

  title = {Principles of {OBJ2}},

2699

  booktitle = {Proceedings of the 12th ACM Symposium on Principles of Programming

2700

	Languages, New Orleans},

2701

  year = {1995},

2702

  pages = {52--66},

2703

  owner = {harald},

2704

  timestamp = {2009.09.18}

2705

2706

2707

@BOOK{Gotz2009,

2708

  title = {iX Studie Modellbasiertes Testen},

2709

  publisher = {Heise Verlag},

2710

  year = {2009},

2711

  author = {Helmut G"{o}tz and Markus Nickolaus and Thomas Ro"sner and Knut Salomon},

2712

  owner = {wkrenn},

2713

  timestamp = {2009.09.17}

2714

2715

2716

@TECHREPORT{Galler2008a,

2717

  author = {Galler, Stefan J. and K\"{o}nigshofer, Robert and Peischl, Bernhard

2718

	and Unterberger, Robert and Wotawa, Franz },

2719

  title = {Automatic Test Generation Tools for Java based on Design-by-Contract(tm):

2720

	A survey},

2721

  institution = {Competence Networt Softnet Austria},

2722

  year = {2008},

2723

  month = {May},

2724

  abstract = {Since testing counts for more than 40\% of total cost of software

2725

	development, automating the software testing process becomes more

2726

	and more important. Therefore, a more formal specification of the

2727

	expected behavior of software components is necessary. The Eiffel

2728

	programming language is the first programming language with built-in

2729

	formal specification of method pre-conditions, post-conditions and

2730

	class invariants, called Design-by-Contract. This technical report

2731

	should give an overview of currently available Design-by-Contract

2732

	specification languages for Java. The focus here is on the practical

2733

	usability of those languages in an real-world industrial project.},

2734

  citeulike-article-id = {2805308},

2735

  keywords = {java, mogentes, testing},

2736

  owner = {harald},

2737

  posted-at = {2008-05-16 14:59:10},

2738

  priority = {2},

2739

  timestamp = {2009.09.18}

2740

2741

2742

@TECHREPORT{Galler2008,

2743

  author = {Galler, Stefan J. and Peischl, Bernhard and Wotawa, Franz},

2744

  title = {Formal Specification Languages for Design-by-Contract in Java: A

2745

	survey},

2746

  institution = {Competence Network Softnet Austria},

2747

  year = {2008},

2748

  key = {SNA-TR-2007-1P3},

2749

  owner = {harald},

2750

  timestamp = {2009.09.18}

2751

2752

2753

@ARTICLE{Gannon1981,

2754

  author = {John Gannon and Paul McMullin and Richard Hamlet},

2755

  title = {Data abstraction implementation, specification and testing},

2756

  journal = {ACM Transactions on Programming Languages and Systems},

2757

  year = {1981},

2758

  volume = {3},

2759

  pages = {211--223},

2760

  number = {3},

2761

  owner = {harald},

2762

  timestamp = {2009.09.18}

2763

2764

2765

@ARTICLE{Garavel2002,

2766

  author = {Hubert Garavel and Fr{\'e}d{\'e}ric Lang and Radu Mateescu},

2767

  title = {An overview of {CADP} 2001},

2768

  journal = {European Association for Software Science and Technology Newsletter},

2769

  year = {2002},

2770

  volume = {4},

2771

  pages = {13-24},

2772

  owner = {harald},

2773

  timestamp = {2009.09.18}

2774

2775

2776

@INPROCEEDINGS{697560,

2777

  author = {Gaudel, Marie-Claude},

2778

  title = {Testing Can Be Formal, Too},

2779

  booktitle = {TAPSOFT '95: Proceedings of the 6th International Joint Conference

2780

	CAAP/FASE on Theory and Practice of Software Development},

2781

  year = {1995},

2782

  pages = {82--96},

2783

  address = {London, UK},

2784

  publisher = {Springer-Verlag},

2785

  isbn = {3-540-59293-8}

2786

2787

2788

@INPROCEEDINGS{Gaudel1995,

2789

  author = {Marie-Claude Gaudel},

2790

  title = {Testing can be formal too},

2791

  booktitle = {TAPSOFT'95: Theory and Practice of Software Development, 6th International

2792

	Joint Conference CAAP/FASE},

2793

  year = {1995},

2794

  volume = {915},

2795

  series = {Lecture Notes in Computer Science},

2796

  pages = {82--96},

2797

  month = {May},

2798

  publisher = {Springer-Verlag},

2799

  owner = {harald},

2800

  timestamp = {2009.09.18}

2801

2802

2803

@INPROCEEDINGS{Gaudel2008,

2804

  author = {Marie-Claude Gaudel and Pascale Le Gall},

2805

  title = {Testing Data Types Implementations from Algebraic Specifications},

2806

  booktitle = {Formal Methods and Testing 2008},

2807

  year = {2008},

2808

  editor = {Robert M. Hierons and Jonathan P. Bowen and Mark Harman},

2809

  volume = {4949},

2810

  series = {LNCS},

2811

  pages = {209--239},

2812

  owner = {harald},

2813

  timestamp = {2009.09.18}

2814

2815

2816

@ARTICLE{Gaudel1998,

2817

  author = {Marie-Claude Gaudel and Perry R.~James},

2818

  title = {Testing Algebraic Data Types and Processes: a Unifying Theory},

2819

  journal = {Formal Aspects of Computing},

2820

  year = {1998},

2821

  volume = {10},

2822

  pages = {436--451},

2823

  number = {5 \& 6},

2824

  libnum = {140},

2825

  owner = {harald},

2826

  timestamp = {2009.09.18}

2827

2828

2829

@BOOK{Glymour1980,

2830

  title = {Theory and Evidence},

2831

  publisher = {Princeton University Press},

2832

  year = {1980},

2833

  author = {Clarke Glymour},

2834

  address = {New Jersey},

2835

  owner = {harald},

2836

  timestamp = {2009.09.18}

2837

2838

2839

@ARTICLE{Glymour1980a,

2840

  author = {Clarke Glymour},

2841

  title = {Hypothetico-deductivism is hopeless},

2842

  journal = {Philosophy of science},

2843

  year = {1980},

2844

  volume = {47},

2845

  pages = {322--325},

2846

  owner = {harald},

2847

  timestamp = {2009.09.18}

2848

2849

2850

@INPROCEEDINGS{Gnesi2004,

2851

  author = {Gnesi, Stefania and Latella, Diego and Massink, Mieke},

2852

  title = {Formal Test-Case Generation for {UML} Statecharts},

2853

  booktitle = {ICECCS '04: Proc. of the 9th IEEE Int. Conf. on Engineering Complex

2854

	Computer Systems Navigating Complexity in the e-Engineering Age},

2855

  year = {2004},

2856

  pages = {75--84},

2857

  publisher = {IEEE Computer Society}

2858

2859

2860

@TECHREPORT{Godefroid2007,

2861

  author = {Godefroid, Patrice and Levin, Michael and Molnar, David },

2862

  title = {Automated Whitebox Fuzz Testing},

2863

  institution = {Microsoft Research},

2864

  year = {2007},

2865

  number = {MSR-TR-2007-58},

2866

  month = {May},

2867

  abstract = {{\\em Fuzz testing} is an effective technique for finding security

2868

	vulnerabilities in software. Traditionally, fuzz testing tools apply

2869

	random mutations to well-formed inputs and test the program on the

2870

	resulting values. We present an alternative {\\em whitebox fuzz testing}

2871

	approach inspired by recent advances in symbolic execution and dynamic

2872

	test generation. Our approach records an actual run of a program

2873

	under test on a well-formed input, symbolically evaluates the recorded

2874

	trace, and generates constraints capturing how the program uses its

2875

	inputs. The generated constraints are used to produce new inputs

2876

	which cause the program to follow different control paths. This process

2877

	is repeated with the help of a code-coverage maximizing heuristic

2878

	designed to find defects as fast as possible. We have implemented

2879

	this algorithm in SAGE (\\emph{Scalable, Automated, Guided Execution}),

2880

	a new tool employing x86 instruction-level tracing and emulation

2881

	for whitebox fuzzing of arbitrary file-reading Windows applications.

2882

	We describe key optimizations needed to make dynamic test generation

2883

	scale to large input files and long execution traces with hundreds

2884

	of millions of instructions. We then present detailed experiments

2885

	with several Windows applications. Notably, without any format-specific

2886

	knowledge, SAGE detects the MS07-017 ANI vulnerability, which was

2887

	missed by extensive blackbox fuzzing and static analysis tools. Furthermore,

2888

	while still in an early stage of development, SAGE has already discovered

2889

	20+ new bugs in large shipped Windows applications including image

2890

	processors, media players, and file decoders. Several of these bugs

2891

	are potentially exploitable memory access violations.},

2892

  citeulike-article-id = {2284715},

2893

  keywords = {bibtex-import},

2894

  owner = {harald},

2895

  posted-at = {2008-01-24 13:13:45},

2896

  priority = {0},

2897

  timestamp = {2009.09.18}

2898

2899

2900

@ARTICLE{Gotlieb1998,

2901

  author = {Gotlieb, Arnaud and Botella, Bernard and Rueher, Michel },

2902

  title = {Automatic test data generation using constraint solving techniques},

2903

  journal = {SIGSOFT Softw. Eng. Notes},

2904

  year = {1998},

2905

  volume = {23},

2906

  pages = {53--62},

2907

  number = {2},

2908

  abstract = {Automatic test data generation leads to identify input values on which

2909

	a selected point in a procedure is ex- ecuted. This paper introduces

2910

	a new method for this problem based on constraint solving techniques.

2911

	First, we statically transform a procedure into a constraint system

2912

	by using well-known "Static Single Assignment" form and control-dependencies.

2913

	Second, we solve this system to check whether at least one feasible

2914

	control flow path going through the selected point exists and to

2915

	generate test data that correspond to one of these paths. The key

2916

	point of our approach is to take advantage of current advances in

2917

	constraint techniques when solving the generated constraint system.

2918

	Global constraints are used in a preliminary step to detect some

2919

	of the non fea- sible paths. Partial consistency techniques are employed

2920

	to reduce the domains of possible values of the test data. A prototype

2921

	implementation has been developped on a restricted subset of the

2922

	C language. Advantages of our approach are illustrated on a non-trivial

2923

	example.},

2924

  address = {New York, NY, USA},

2925

  citeulike-article-id = {2638008},

2926

  doi = {http://doi.acm.org/10.1145/271775.271790},

2927

  keywords = {bibtex-import, execution, generation, symbolic, test, vector},

2928

  local-url = {file://localhost/Users/michele/mogentes/bibliography/p53-gotlieb.pdf},

2929

  owner = {harald},

2930

  posted-at = {2008-04-07 16:23:44},

2931

  priority = {2},

2932

  publisher = {ACM},

2933

  timestamp = {2009.09.18},

2934

  url = {http://dx.doi.org/10.1145/271775.271790}

2935

2936

2937

@TECHREPORT{Grabowski1999,

2938

  author = {Jens Grabowski and Dieter Hogrefe},

2939

  title = {{The Standardization of Core INAP CS-2 by ETSI}},

2940

  institution = {Technical Report A-99-02, Medical University of L\"{u}beck, Schriftenreihe

2941

	der Institute f\"{u}r Mathematik/Informatik, L\"{u}beck, February

2942

	1999},

2943

  year = {1999},

2944

  month = feb,

2945

  keywords = {SDL, MSC, TTCN, ASN.1, conformance testing, automatic test generation,

2946

	standardization, ETSI, ITU-T},

2947

  owner = {harald},

2948

  timestamp = {2009.09.18}

2949

2950

2951

@ARTICLE{Grieskamp2010,

2952

  author = {Wolfgang Grieskamp and Nicolas Kicillof and Keith Stobie and Victor

2953

	Braberman},

2954

  title = {Model-based quality assurance of protocol documentation: tools and

2955

	methodology},

2956

  journal = {Software Testing, Verification and Reliability (STVR)},

2957

  year = {2010},

2958

  owner = {harald},

2959

  timestamp = {2011.01.11}

2960

2961

2962

@ARTICLE{Grieskamp2006,

2963

  author = {Wolfgang Grieskamp and Nicolas Kicillof and Nikolai Tillmann},

2964

  title = {Action Machines: a Framework for Encoding and Composing Partial Behaviors},

2965

  journal = {International Journal of Software Engineering and Knowledge Engineering},

2966

  year = {2006},

2967

  volume = {16},

2968

  pages = {705-726},

2969

  number = {5},

2970

  bibsource = {DBLP, http://dblp.uni-trier.de},

2971

  ee = {http://dx.doi.org/10.1142/S0218194006002963},

2972

  owner = {harald},

2973

  timestamp = {2009.09.18}

2974

2975

2976

@INPROCEEDINGS{Griesmayer2009,

2977

  author = {Andreas Griesmayer and Bernhard K. Aichernig and Einar Broch Johnsen

2978

	and Rudolf Schlatte},

2979

  title = {Dynamic Symbolic Execution for Testing Distributed Objects},

2980

  booktitle = {TAP},

2981

  year = {2009},

2982

  pages = {105-120},

2983

  bibsource = {DBLP, http://dblp.uni-trier.de},

2984

  ee = {http://dx.doi.org/10.1007/978-3-642-02949-3_9}

2985

2986

2987

@BOOK{Group1992,

2988

  title = {The RAISE Specification Language},

2989

  publisher = {Prentice-Hall},

2990

  year = {1992},

2991

  author = {The RAISE Language Group},

2992

  series = {The BCS Practitioners Series},

2993

  owner = {harald},

2994

  timestamp = {2009.09.18}

2995

2996

2997

@BOOK{Group1995,

2998

  title = {The RAISE Development Method},

2999

  publisher = {Prentice-Hall},

3000

  year = {1995},

3001

  author = {The RAISE Method Group},

3002

  series = {The BCS Practitioners Series},

3003

  owner = {harald},

3004

  timestamp = {2009.09.18}

3005

3006

3007

@ARTICLE{Gupta2000,

3008

  author = {Gupta, N. and Mathur, A. P. and Soffa, M. L. },

3009

  title = {Generating test data for branch coverage},

3010

  journal = {Automated Software Engineering, 2000. Proceedings ASE 2000. The Fifteenth

3011

	IEEE International Conference on},

3012

  year = {2000},

3013

  pages = {219--227},

3014

  abstract = {Branch coverage is an important criteria used during the structural

3015

	testing of programs. In this paper, we present a new program execution

3016

	based approach to generate input data that exercises a selected branch

3017

	in a program. The test data generation is initiated with an arbitrarily

3018

	chosen input from the input domain of the program. A new input is

3019

	derived from the initial input in an attempt to force execution through

3020

	any of the paths through the selected branch. The method dynamically

3021

	switches among the paths that reach the branch by refining the input.

3022

	Using a numerical iterative technique that attempts to generate an

3023

	input to exercise the branch, it dynamically selects Q path that

3024

	offers less resistance. We have implemented the technique and present

3025

	experimental results of its performance for some programs. Our results

3026

	show that our method is feasible and practical.},

3027

  citeulike-article-id = {2638009},

3028

  doi = {10.1109/ASE.2000.873666},

3029

  keywords = {bibtex-import, branch, coverage, generation, program, structural,

3030

	test, testing, vector},

3031

  local-url = {file://localhost/Users/michele/mogentes/bibliography/00873666.pdf},

3032

  owner = {harald},

3033

  posted-at = {2008-04-07 16:23:44},

3034

  priority = {2},

3035

  timestamp = {2009.09.18},

3036

  url = {http://dx.doi.org/10.1109/ASE.2000.873666}

3037

3038

3039

@ARTICLE{Gupta1998,

3040

  author = {Gupta, Neelam and Mathur, Aditya P. and Soffa, Mary L. },

3041

  title = {Automated test data generation using an iterative relaxation method},

3042

  journal = {SIGSOFT Softw. Eng. Notes},

3043

  year = {1998},

3044

  volume = {23},

3045

  pages = {231--244},

3046

  number = {6},

3047

  abstract = {An important problem that arises in path oriented testing is the generation

3048

	of test data that causes a program to follow a given path. In this

3049

	paper, we present a novel program execution based approach using

3050

	an iterative relaxation method to address the above problem. In this

3051

	method, test data generation is initiated with an arbitrarily chosen

3052

	input from a given domain. This input is then iteratively refined

3053

	to obtain an input on which all the branch predicates on the given

3054

	path evaluate to the desired outcome. In each iteration the program

3055

	statements relevant to the evaluation of each branch predicate on

3056

	the path are executed, and a set of linear constraints is derived.

3057

	The constraints are then solved to obtain the increments for the

3058

	input. These increments are added to the current input to obtain

3059

	the input for the next iteration. The relaxation technique used in

3060

	deriving the constraints provides feedback on the amount by which

3061

	each input variable should be adjusted for the branches on the path

3062

	to evaluate to the desired outcome.When the branch conditions on

3063

	a path are linear functions of input variables, our technique either

3064

	finds a solution for such paths in one iteration or it guarantees

3065

	that the path is infeasible. In contrast, existing execution based

3066

	approaches may require an unacceptably large number of iterations

3067

	for relatively long paths because they consider only one input variable

3068

	and one branch predicate at a time and use backtracking. When the

3069

	branch conditions on a path are nonlinear functions of input variables,

3070

	though it may take more then one iteration to derive a desired input,

3071

	the set of constraints to be solved in each iteration is linear and

3072

	is solved using Gaussian elimination. This makes our technique practical

3073

	and suitable for automation.},

3074

  address = {New York, NY, USA},

3075

  citeulike-article-id = {2638001},

3076

  doi = {http://doi.acm.org/10.1145/291252.288321},

3077

  keywords = {bibtex-import},

3078

  local-url = {file://localhost/Users/michele/mogentes/bibliography/p231-gupta.pdf},

3079

  owner = {harald},

3080

  posted-at = {2008-04-07 16:23:43},

3081

  priority = {2},

3082

  publisher = {ACM},

3083

  timestamp = {2009.09.18},

3084

  url = {http://dx.doi.org/10.1145/291252.288321}

3085

3086

3087

@ARTICLE{Gurevich2000,

3088

  author = {Yuri Gurevich},

3089

  title = {Sequential abstract-state machines capture sequential algorithms},

3090

  journal = {ACM Trans. Comput. Logic},

3091

  year = {2000},

3092

  volume = {1},

3093

  pages = {77--111},

3094

  number = {1},

3095

  address = {New York, NY, USA},

3096

  doi = {http://doi.acm.org/10.1145/343369.343384},

3097

  issn = {1529-3785},

3098

  owner = {harald},

3099

  publisher = {ACM},

3100

  timestamp = {2009.09.18}

3101

3102

3103

@ARTICLE{Guttag1977,

3104

  author = {J.~Guttag},

3105

  title = {Abstract Data Types and the Development of Data Structures},

3106

  journal = {Communications of the ACM},

3107

  year = {1977},

3108

  volume = {20},

3109

  pages = {369--405},

3110

  number = {6},

3111

  owner = {harald},

3112

  timestamp = {2009.09.18}

3113

3114

3115

@ARTICLE{Guttag1985,

3116

  author = {J.V.~Guttag and J.J.~Horning and J.M.~Wing},

3117

  title = {The {Larch} family of specification languages},

3118

  journal = {IEEE Software},

3119

  year = {1985},

3120

  volume = {2},

3121

  pages = {24--36},

3122

  number = {5},

3123

  owner = {harald},

3124

  timestamp = {2009.09.18}

3125

3126

3127

@BOOK{Guttag1993,

3128

  title = {{Larch}: Languages and Tools for Formal Specification},

3129

  publisher = {Springer Verlag},

3130

  year = {1993},

3131

  author = {John V.~Guttag and James J.~Horning},

3132

  series = {Texts and Monographs in Computer Science},

3133

  owner = {harald},

3134

  timestamp = {2009.09.18}

3135

3136

3137

@INPROCEEDINGS{Haeberer2001,

3138

  author = {A. M. Haeberer and T. S. E. Maibaum},

3139

  title = {{Scientific rigour, an answer to a pragmatic question: a linguistic

3140

	framework for software engineering}},

3141

  booktitle = {Proceedings of the 23rd International Conference on Software engineering,

3142

	Toronto, Ontario, Canada},

3143

  year = {2001},

3144

  pages = {463--472},

3145

  publisher = {IEEE Computer Society},

3146

  owner = {harald},

3147

  timestamp = {2009.09.18}

3148

3149

3150

@ARTICLE{Halbwachs1991,

3151

  author = {N. Halbwachs and P. Caspi and P. Raymond and D. Pilaud},

3152

  title = {The synchronous data-flow programming language {LUSTRE}},

3153

  journal = {Proceedings of the IEEE},

3154

  year = {1991},

3155

  volume = {79},

3156

  pages = {1305--1320},

3157

  number = {9},

3158

  month = {September},

3159

  owner = {harald},

3160

  timestamp = {2009.09.18},

3161

  url = {citeseer.ist.psu.edu/halbwachs91synchronous.html}

3162

3163

3164

@ARTICLE{Harder3-10May2003,

3165

  author = {Harder, M. and Mellen, J. and Ernst, M. D. },

3166

  title = {Improving test suites via operational abstraction},

3167

  journal = {Software Engineering, 2003. Proceedings. 25th International Conference

3168

	on},

3169

  year = {3-10 May 2003},

3170

  pages = {60--71},

3171

  abstract = {This paper presents the operational difference technique for generating,

3172

	augmenting, and minimizing test suites. The technique is analogous

3173

	to structural code coverage techniques, but it operates in the semantic

3174

	domain of program properties rather than the syntactic domain of

3175

	program text. The operational difference technique automatically

3176

	selects test cases; it assumes only the existence of a source of

3177

	test cases. The technique dynamically generates operational abstractions

3178

	(which describe observed behavior and are syntactically identical

3179

	to formal specifications)from test suite executions. Test suites

3180

	can be generated by adding cases until the operational abstraction

3181

	stops changing. The resulting test suites are as small, and detect

3182

	as many faults, as suites with 100 branch coverage, and are better

3183

	at detecting certain common faults. This paper also presents the

3184

	area and stacking techniques for comparing test suite generation

3185

	strategies; these techniques avoid bias due to test suite size.},

3186

  citeulike-article-id = {2638000},

3187

  doi = {10.1109/ICSE.2003.1201188},

3188

  keywords = {abstractions, bibtex-import, code, coverage, difference, domain, executions,

3189

	formal, generation, language, operational, program, programming,

3190

	semantics, specification, specifications, stacking, strategies, structural,

3191

	suite, syntactic, technique, techniques, test, testing, text, verification},

3192

  local-url = {file://localhost/Users/michele/mogentes/bibliography/improve-testsuite-icse2003.pdf},

3193

  owner = {harald},

3194

  posted-at = {2008-04-07 16:23:43},

3195

  priority = {2},

3196

  timestamp = {2009.09.18},

3197

  url = {http://dx.doi.org/10.1109/ICSE.2003.1201188}

3198

3199

3200

@ARTICLE{Harel1987,

3201

  author = {David Harel},

3202

  title = {Statecharts: {A} Visual Formalism for Complex Systems},

3203

  journal = {Science of Computer Programming},

3204

  year = {1987},

3205

  volume = {8},

3206

  pages = {231--274},

3207

  number = {3},

3208

  month = {June},

3209

  owner = {harald},

3210

  timestamp = {2009.09.18},

3211

  url = {citeseer.ist.psu.edu/harel87statecharts.html}

3212

3213

3214

@ARTICLE{Harel1987a,

3215

  author = {David Harel},

3216

  title = {Statecharts: A visual formalism for complex systems},

3217

  journal = {Sci. Comput. Program.},

3218

  year = {1987},

3219

  volume = {8},

3220

  pages = {231--274},

3221

  number = {3},

3222

  address = {Amsterdam, The Netherlands, The Netherlands},

3223

  doi = {http://dx.doi.org/10.1016/0167-6423(87)90035-9},

3224

  issn = {0167-6423},

3225

  owner = {harald},

3226

  publisher = {Elsevier North-Holland, Inc.},

3227

  timestamp = {2009.09.18}

3228

3229

3230

@TECHREPORT{Hartman2004,

3231

  author = {Alan Hartman},

3232

  title = {Final Project Report},

3233

  institution = {AGEDIS},

3234

  year = {2004},

3235

  month = {February},

3236

  owner = {harald},

3237

  timestamp = {2009.09.18}

3238

3239

3240

@INPROCEEDINGS{Hartmann2000,

3241

  author = {Jean Hartmann and Claudio Imoberdorf and Michael Meisinger},

3242

  title = {UML-Based integration testing},

3243

  booktitle = {ISSTA},

3244

  year = {2000},

3245

  pages = {60-70},

3246

  bibsource = {DBLP, http://dblp.uni-trier.de},

3247

  ee = {http://doi.acm.org/10.1145/347324.348872},

3248

  owner = {harald},

3249

  timestamp = {2009.09.18}

3250

3251

3252

@ARTICLE{Hartmann2005,

3253

  author = {Jean Hartmann and Marlon Vieira and Herbert Foster and Axel Ruder},

3254

  title = {A UML-based approach to system testing},

3255

  journal = {ISSE},

3256

  year = {2005},

3257

  volume = {1},

3258

  pages = {12-24},

3259

  number = {1},

3260

  bibsource = {DBLP, http://dblp.uni-trier.de},

3261

  ee = {http://dx.doi.org/10.1007/s11334-005-0006-0},

3262

  owner = {harald},

3263

  timestamp = {2009.09.18}

3264

3265

3266

@ARTICLE{Hennessy1985,

3267

  author = {Matthew Hennessy and Robin Milner},

3268

  title = {Algebraic laws for nondeterminism and concurrency},

3269

  journal = {J. ACM},

3270

  year = {1985},

3271

  volume = {32},

3272

  pages = {137--161},

3273

  number = {1},

3274

  address = {New York, NY, USA},

3275

  doi = {10.1145/2455.2460},

3276

  issn = {0004-5411},

3277

  owner = {harald},

3278

  publisher = {ACM Press},

3279

  timestamp = {2009.09.18}

3280

3281

3282

@INPROCEEDINGS{Henzinger1996,

3283

  author = {T. A. Henzinger},

3284

  title = {The theory of hybrid automata},

3285

  booktitle = {LICS '96: Proceedings of the 11th Annual IEEE Symposium on Logic

3286

	in Computer Science},

3287

  year = {1996},

3288

  pages = {278},

3289

  address = {Washington, DC, USA},

3290

  publisher = {IEEE Computer Society},

3291

  isbn = {0-8186-7463-6},

3292

  owner = {harald},

3293

  timestamp = {2009.09.18}

3294

3295

3296

@INPROCEEDINGS{Henzinger1997,

3297

  author = {Henzinger, Thomas A. and Ho, Pei-Hsin and Wong-Toi, Howard},

3298

  title = {HYTECH: A Model Checker for Hybrid Systems},

3299

  booktitle = {CAV '97: Proceedings of the 9th International Conference on Computer

3300

	Aided Verification},

3301

  year = {1997},

3302

  pages = {460--463},

3303

  address = {London, UK},

3304

  publisher = {Springer-Verlag},

3305

  isbn = {3-540-63166-6}

3306

3307

3308

@INPROCEEDINGS{Henzinger2000,

3309

  author = {Thomas A. Henzinger and Benjamin Horowitz and Rupak Majumdar and

3310

	Howard Wong-toi},

3311

  title = {Beyond HYTECH: Hybrid systems analysis using interval numerical methods},

3312

  booktitle = {in HSCC},

3313

  year = {2000},

3314

  pages = {130--144},

3315

  publisher = {Springer}

3316

3317

3318

@INPROCEEDINGS{Henzinger2002,

3319

  author = {Henzinger, Thomas A. and Jhala, Ranjit and Majumdar, Rupak and Sutre,

3320

	Gr\'{e}goire },

3321

  title = {Lazy abstraction},

3322

  booktitle = {POPL '02: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on

3323

	Principles of programming languages},

3324

  year = {2002},

3325

  pages = {58--70},

3326

  address = {New York, NY, USA},

3327

  publisher = {ACM},

3328

  abstract = {One approach to model checking software is based on the abstract-check-refine

3329

	paradigm: build an abstract model, then check the desired property,

3330

	and if the check fails, refine the model and start over. We introduce

3331

	the concept of lazy abstraction to integrate and optimize the three

3332

	phases of the abstract-cheek-refine loop. Lazy abstraction continuously

3333

	builds and refines a single abstract model on demand, driven by the

3334

	model checker, so that different parts of the model may exhibit different

3335

	degrees of precision, namely just enough to verify the desired property.

3336

	We present an algorithm for model checking safety properties using

3337

	lazy abstraction and describe an implementation of the algorithm

3338

	applied to C programs. We also provide sufficient conditions for

3339

	the termination of the method.},

3340

  citeulike-article-id = {2638014},

3341

  doi = {http://doi.acm.org/10.1145/503272.503279},

3342

  keywords = {bibtex-import, blast},

3343

  local-url = {file://localhost/Users/michele/mogentes/bibliography/p58-henzinger.pdf},

3344

  owner = {harald},

3345

  posted-at = {2008-04-07 16:23:45},

3346

  priority = {2},

3347

  timestamp = {2009.09.18},

3348

  url = {http://dx.doi.org/10.1145/503272.503279}

3349

3350

3351

@INPROCEEDINGS{Henzinger1995,

3352

  author = {Henzinger, Thomas A. and Kopke, Peter W. and Puri, Anuj and Varaiya,

3353

	Pravin},

3354

  title = {What's decidable about hybrid automata?},

3355

  booktitle = {STOC '95: Proceedings of the twenty-seventh annual ACM symposium

3356

	on Theory of computing},

3357

  year = {1995},

3358

  pages = {373--382},

3359

  address = {New York, NY, USA},

3360

  publisher = {ACM},

3361

  doi = {http://doi.acm.org/10.1145/225058.225162},

3362

  isbn = {0-89791-718-9},

3363

  location = {Las Vegas, Nevada, United States}

3364

3365

3366

@INPROCEEDINGS{Hessel2004,

3367

  author = {Anders Hessel and Paul Pettersson},

3368

  title = {A Test Case Generation Algorithm for Real-Time Systems},

3369

  booktitle = {QSIC '04: Proceedings of the Quality Software, Fourth International

3370

	Conference},

3371

  year = {2004},

3372

  pages = {268--273},

3373

  address = {Washington, DC, USA},

3374

  publisher = {IEEE Computer Society},

3375

  doi = {http://dx.doi.org/10.1109/QSIC.2004.5},

3376

  isbn = {0-7695-2207-6},

3377

  owner = {harald},

3378

  timestamp = {2009.09.18}

3379

3380

3381

@INPROCEEDINGS{Hickey2004,

3382

  author = {Timothy J. Hickey and David K. Wittenberg},

3383

  title = {Rigorous Modeling of Hybrid Systems Using Interval Arithmetic Constraints},

3384

  booktitle = {HSCC},

3385

  year = {2004},

3386

  pages = {402-416},

3387

  owner = {harald},

3388

  timestamp = {2009.09.18},

3389

  url = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2993{\&}spage=402}

3390

3391

3392

@ARTICLE{Hierons2009,

3393

  author = {Robert M. Hierons and Kirill Bogdanov and Jonathan P. Bowen and Rance

3394

	Cleaveland and John Derrick and Jeremy Dick and Marian Gheorghe and

3395

	Mark Harman and Kalpesh Kapoor and Paul Krause and Gerald L{\"u}ttgen

3396

	and Anthony J. H. Simons and Sergiy A. Vilkomir and Martin R. Woodward

3397

	and Hussein Zedan},

3398

  title = {Using formal specifications to support testing},

3399

  journal = {ACM Computing Surveys},

3400

  year = {2009},

3401

  volume = {41},

3402

  number = {2},

3403

  bibsource = {DBLP, http://dblp.uni-trier.de},

3404

  ee = {http://doi.acm.org/10.1145/1459352.1459354},

3405

  owner = {harald},

3406

  timestamp = {2009.09.18}

3407

3408

3409

@INPROCEEDINGS{Hierons2008a,

3410

  author = {Hierons, Robert M. and Merayo, Mercedes G. and N, Manuel},

3411

  title = {Implementation Relations for the Distributed Test Architecture},

3412

  booktitle = {TestCom '08 / FATES '08: Proceedings of the 20th IFIP TC 6/WG 6.1

3413

	international conference on Testing of Software and Communicating

3414

	Systems},

3415

  year = {2008},

3416

  pages = {200--215},

3417

  address = {Berlin, Heidelberg},

3418

  publisher = {Springer-Verlag},

3419

  doi = {http://dx.doi.org/10.1007/978-3-540-68524-1_15},

3420

  isbn = {978-3-540-68514-2},

3421

  location = {Tokyo, Japan}

3422

3423

3424

@BOOK{Hoare1985,

3425

  title = {Communicating Sequential Processes},

3426

  publisher = {Prentice-Hall},

3427

  year = {1985},

3428

  author = {C.A.R. Hoare},

3429

  series = {International Series in Computer Science},

3430

  owner = {harald},

3431

  timestamp = {2009.09.18}

3432

3433

3434

@ARTICLE{Hoare1978,

3435

  author = {Hoare, CAR},

3436

  title = {{Communicating sequential processes}},

3437

  journal = {Communications of the ACM},

3438

  year = {1978},

3439

  volume = {21},

3440

  pages = {666--677},

3441

  number = {8},

3442

  owner = {harald},

3443

  publisher = {ACM Press New York, NY, USA},

3444

  timestamp = {2009.09.18}

3445

3446

3447

@ARTICLE{Hoare1969,

3448

  author = {Hoare, C. A. R.},

3449

  title = {An Axiomatic Basis for Computer Programming},

3450

  journal = {Communications of the ACM},

3451

  year = {1969},

3452

  volume = {12},

3453

  pages = {576--580 and 583},

3454

  number = {10},

3455

  month = {October},

3456

  owner = {harald},

3457

  timestamp = {2009.09.18}

3458

3459

3460

@BOOK{Hoare1998,

3461

  title = {Unifying Theories of Programming},

3462

  publisher = {Prentice-Hall International},

3463

  year = {1998},

3464

  author = {C.A.R.~Hoare and He Jifeng},

3465

  key = {HH98},

3466

  owner = {harald},

3467

  timestamp = {2009.09.18}

3468

3469

3470

@INPROCEEDINGS{Holzer2008,

3471

  author = {Andreas Holzer and Christian Schallhart and Michael Tautschnig and

3472

	Helmut Veith},

3473

  title = {{FShell: Systematic Test Case Generation for Dynamic Analysis and

3474

	Measurement}},

3475

  booktitle = {Proceedings of the 20th International Conference on Computer Aided

3476

	Verification (CAV 2008)},

3477

  year = {2008},

3478

  volume = {5123},

3479

  series = {Lecture Notes in Computer Science},

3480

  pages = {209--213},

3481

  address = {Princeton, NJ, USA},

3482

  month = JUL,

3483

  publisher = {Springer},

3484

  owner = {harald},

3485

  timestamp = {2009.09.18}

3486

3487

3488

@BOOK{Holzmann2004,

3489

  title = {{The Spin Model Checker: Primer and Reference Manual}},

3490

  publisher = {Addison-Wesley Professional},

3491

  year = {2004},

3492

  author = {Holzmann, G.J.},

3493

  owner = {harald},

3494

  timestamp = {2009.09.18}

3495

3496

3497

@ARTICLE{Holzmann1997,

3498

  author = {Gerard J. Holzmann},

3499

  title = {{The Model Checker SPIN}},

3500

  journal = {IEEE Trans. Softw. Eng.},

3501

  year = {1997},

3502

  volume = {23},

3503

  pages = {279--295},

3504

  number = {5},

3505

  address = {Piscataway, NJ, USA},

3506

  doi = {10.1109/32.588521},

3507

  issn = {0098-5589},

3508

  owner = {harald},

3509

  publisher = {IEEE Press},

3510

  timestamp = {2009.09.18}

3511

3512

3513

@ARTICLE{Hong2003,

3514

  author = {Hong, Hyoung S. and Cha, Sung D. and Lee, Insup and Sokolsky, Oleg

3515

	and Ural, Hasan},

3516

  title = {Data Flow Testing as Model Checking},

3517

  journal = {icse},

3518

  year = {2003},

3519

  volume = {00},

3520

  pages = {232},

3521

  abstract = {This paper presents a model checking-based approach to data flow testing.

3522

	We characterize data flow oriented coverage criteria in temporal

3523

	logic such that the problem of test generation is reduced to the

3524

	problem of finding witnesses for a set of temporal logic formulas.

3525

	The capability of model checkers to construct witnesses and counterexamples

3526

	allows test generation to be fully automatic. We discuss complexity

3527

	issues in minimal cost test generation and describe heurstic test

3528

	generation algorithms. We illustrate our approach using CTL as temporal

3529

	logic and SMV as model checker.},

3530

  address = {Los Alamitos, CA, USA},

3531

  citeulike-article-id = {2638002},

3532

  doi = {http://doi.ieeecomputersociety.org/10.1109/ICSE.2003.1201203},

3533

  keywords = {bibtex-import, coverage, criteria},

3534

  local-url = {file://localhost/Users/michele/mogentes/bibliography/03icse.pdf},

3535

  owner = {harald},

3536

  posted-at = {2008-04-07 16:23:43},

3537

  priority = {2},

3538

  publisher = {IEEE Computer Society},

3539

  timestamp = {2009.09.18},

3540

  url = {http://dx.doi.org/http://doi.ieeecomputersociety.org/10.1109/ICSE.2003.1201203}

3541

3542

3543

@BOOK{Horebeek1993,

3544

  title = {Algebraic Specifications in Software Engineering, an Introduction},

3545

  publisher = {Springer Verlag},

3546

  year = {1993},

3547

  author = {Ivo Van Horebeek and Johan Lewi},

3548

  owner = {harald},

3549

  timestamp = {2009.09.18}

3550

3551

3552

@ARTICLE{HowdenSept.1976,

3553

  author = {Howden, W. E. },

3554

  title = {Reliability of the Path Analysis Testing Strategy},

3555

  journal = {Software Engineering, Transactions on},

3556

  year = {Sept. 1976},

3557

  volume = {SE-2},

3558

  pages = {208--215},

3559

  number = {3},

3560

  abstract = {A set of test data T for a program P is reliable if it reveals that

3561

	P contains an error whenever P is incorrect. If a set of tests T

3562

	is reliable and P produces the correct output for each element of

3563

	T then P is a correct program. Test data generation strategies are

3564

	procedures for generating sets of test data. A testing strategy is

3565

	reliable for a program P if it produces a reliable set of test data

3566

	for P. It is proved that an effective testing strategy which is reliable

3567

	for all programs cannot be constructed. A description of the path

3568

	analysis testing strategy is presented. In the path analysis strategy

3569

	data are generated which cause different paths in a program to be

3570

	executed. A method for analyzing the reliability of path testing

3571

	is introduced. The method is used to characterize certain classes

3572

	of programs and program errors for which the path analysis strategy

3573

	is reliable. Examples of published incorrect programs are included.},

3574

  citeulike-article-id = {2637999},

3575

  keywords = {analysissymbolic, bibtex-import, execution, path},

3576

  local-url = {file://localhost/Users/michele/mogentes/bibliography/01702367.pdf},

3577

  owner = {harald},

3578

  posted-at = {2008-04-07 16:23:42},

3579

  priority = {2},

3580

  timestamp = {2009.09.18}

3581

3582

3583

@ELECTRONIC{ConferenceProtocol,

3584

  author = {http://fmt.cs.utwente.nl/ConfCase/v1.00/description/confprot.html},

3585

  title = {Conference Protocol},

3586

  url = {http://fmt.cs.utwente.nl/ConfCase/v1.00/description/confprot.html},

3587

  owner = {harald},

3588

  timestamp = {2009.06.22}

3589

3590

3591

@ELECTRONIC{EventB,

3592

  author = {http://www.event-b.org/},

3593

  title = {Event-B},

3594

  url = {http://www.event-b.org/},

3595

  owner = {harald},

3596

  timestamp = {2009.06.22}

3597

3598

3599

@ARTICLE{IEEE2Sep1998,

3600

  author = {IEEE},

3601

  title = {IEEE standard for information technology - requirements and guidelines

3602

	for test methods specifications and test method implementations for

3603

	measuring conformance to POSIX(R) standards},

3604

  journal = {IEEE Std 2003-1997},

3605

  year = {2 Sep 1998},

3606

  pages = {-},

3607

  keywords = {IEEE standards, Unix, application program interfaces, conformance

3608

	testing, formal specification, information technology, program testing,

3609

	software standardsAPI standards, IEEE Std 2003-1997, IEEE standard,

3610

	POSIX standards, application programming interface, assertion test,

3611

	conformance document, conformance measurement, conformance test procedure,

3612

	conformance test software, implementation under test, information

3613

	technology, options, specification standards, test method implementations,

3614

	test method specifications, test result code},

3615

  owner = {harald},

3616

  timestamp = {2009.09.18}

3617

3618

3619

@ARTICLE{IEEE1990,

3620

  author = {IEEE},

3621

  title = {{IEEE} Standard Glossary of Software Engineering Terminology},

3622

  journal = {IEEE Std 610.12-1990},

3623

  year = {1990},

3624

  month = Dec,

3625

  biburl = {http://www.bibsonomy.org/bibtex/2168c4ff010eecef4cce9d5b0030060ce/wiljami74},

3626

  keywords = {IEEE_Standard}

3627

3628

3629

@MISC{ISO1997,

3630

  author = {ISO},

3631

  title = {Information processing systems --- {Open} systems interconnection

3632

	--- {Estelle} --- A formal description technique based on an extended

3633

	state transition model},

3634

  year = {1997},

3635

  address = {Geneva},

3636

  number = {9074},

3637

  organization = {International Organization for Standardization},

3638

  owner = {harald},

3639

  timestamp = {2009.09.18},

3640

  type = {IS}

3641

3642

3643

@MISC{ISO1989,

3644

  author = {ISO},

3645

  title = {{ISO} 8807: Information processing systems -- Open Systems Interconnection

3646

	-- {LOTOS} -- A formal description technique based on the temporal

3647

	ordering of observational behaviour},

3648

  year = {1989},

3649

  comment = {r},

3650

  file = {iso1989lotos.pdf:iso1989lotos.pdf:PDF},

3651

  institution = {iso.ch},

3652

  owner = {martin},

3653

  timestamp = {2007.09.07}

3654

3655

3656

@BOOK{ISO/IEC2002,

3657

  title = {Z formal specification notation -- Syntax, type system and semantics},

3658

  publisher = {ISO/IEC},

3659

  year = {2002},

3660

  author = {ISO/IEC},

3661

  owner = {harald},

3662

  timestamp = {2009.09.18}

3663

3664

3665

@MISC{ITU-T2002,

3666

  author = {ITU-T},

3667

  title = {{Formal description techniques (FDT) -- Specification and Description

3668

	Language (SDL)}},

3669

  year = {2002},

3670

  owner = {harald},

3671

  timestamp = {2009.09.18}

3672

3673

3674

@INPROCEEDINGS{J'eron1999,

3675

  author = {J\'{e}ron, Thierry and Morel, Pierre},

3676

  title = {Test Generation Derived from Model-Checking},

3677

  booktitle = {CAV '99: Proceedings of the 11th International Conference on Computer

3678

	Aided Verification},

3679

  year = {1999},

3680

  pages = {108--121},

3681

  address = {London, UK},

3682

  publisher = {Springer-Verlag},

3683

  isbn = {3-540-66202-2}

3684

3685

3686

@BOOK{Jackson2006,

3687

  title = {Software Abstractions: Logic, Language, and Analysis},

3688

  publisher = {The MIT Press},

3689

  year = {2006},

3690

  author = {Daniel Jackson},

3691

  isbn = {0262101149},

3692

  owner = {harald},

3693

  timestamp = {2009.09.18}

3694

3695

3696

@ARTICLE{Jackson2000,

3697

  author = {Jackson, Daniel and Vaziri, Mandana },

3698

  title = {Finding bugs with a constraint solver},

3699

  journal = {SIGSOFT Softw. Eng. Notes},

3700

  year = {2000},

3701

  volume = {25},

3702

  pages = {14--25},

3703

  number = {5},

3704

  abstract = {A method for finding bugs in code is presented. For given small numbers

3705

	j and k, the code of a procedure is translated into a relational

3706

	formula whose models represent all execution traces that involve

3707

	at most j heap cells and k loop iterations. This formula is conjoined

3708

	with the negation of the procedure's specification. The models of

3709

	the resulting formula, obtained using a constraint solver, are counterexamples:

3710

	executions of the code that violate the specification. The method

3711

	can analyze millions of executions in seconds, and thus rapidly expose

3712

	quite subtle flaws. It can accommodate calls to procedures for which

3713

	specifications but no code is available. A range of standard properties

3714

	(such as absence of null pointer dereferences) can also be easily

3715

	checked, using predefined specifications.},

3716

  address = {New York, NY, USA},

3717

  citeulike-article-id = {2638006},

3718

  doi = {http://doi.acm.org/10.1145/347636.383378},

3719

  keywords = {bibtex-import, boundingsymbolic, execution, loop},

3720

  local-url = {file://localhost/Users/michele/mogentes/bibliography/p14-jackson.pdf},

3721

  owner = {harald},

3722

  posted-at = {2008-04-07 16:23:44},

3723

  priority = {2},

3724

  publisher = {ACM},

3725

  timestamp = {2009.09.18},

3726

  url = {http://dx.doi.org/10.1145/347636.383378}

3727

3728

3729

@ARTICLE{Jacobs2001,

3730

  author = {Bart Jacobs},

3731

  title = {Assertional and Behavioural Refinement in Coalgebraic Specification},

3732

  journal = {Electronic Notes in Theoretical Computer Science},

3733

  year = {2001},

3734

  volume = {47},

3735

  pages = {1--36},

3736

  libnum = {178},

3737

  owner = {harald},

3738

  timestamp = {2009.09.18}

3739

3740

3741

@ARTICLE{Jard2005,

3742

  author = {Claude Jard and Thierry J{\'e}ron},

3743

  title = {{TGV}: theory, principles and algorithms},

3744

  journal = {International Journal on Software Tools for Technology Transfer},

3745

  year = {2005},

3746

  volume = {7},

3747

  pages = {297-315},

3748

  number = {4},

3749

  month = {August},

3750

  abstract = {This paper discusses the details of the tool TGV. TGV operates on

3751

	a Input/Output-Labeled Transition System (IOLTS) for the specification

3752

	and an IOLTS for a test purpose. On the construction of the intersection

3753

	of this IOLTS TGV generates a Test-Case Graph. This Test-Case Graph

3754

	is again an IOLTS. Based on the input/output conformance relation

3755

	the Test-Case Graph can be used to generate a verdict for a certain

3756

	Implementation under Test},

3757

  comment = {p,r},

3758

  file = {jard2005tgv.pdf:jard2005tgv.pdf:PDF},

3759

  filename = {./test\_generation/Jard-Jeron-05.ps},

3760

  keywords = {Testing, Conformance Test, Test generation, Input/Output Labeled Transition

3761

	System},

3762

  owner = {martin},

3763

  timestamp = {2007.07.27}

3764

3765

3766

@INPROCEEDINGS{Jasper1994,

3767

  author = {Jasper, Robert and Brennan, Mike and Williamson, Keith and Currier,

3768

	Bill and Zimmerman, David },

3769

  title = {Test data generation and feasible path analysis},

3770

  booktitle = {ISSTA '94: Proceedings of the 1994 ACM SIGSOFT international symposium

3771

	on Software testing and analysis},

3772

  year = {1994},

3773

  pages = {95--107},

3774

  address = {New York, NY, USA},

3775

  publisher = {ACM},

3776

  abstract = {This paper describes techniques used by Test Specification and Determination

3777

	Tool (TSDT), an experimental prototype for analysis and testing of

3778

	critical applications written in Ada. Two problems dominate structural

3779

	testing of programs: exponential explosion in the number of execution

3780

	paths and feasible path determination, A path is feasible if there

3781

	exists some input that will cause the path to be traversed during

3782

	execution. We present techniques based on new representations combined

3783

	with automated theorem proving to deal with these problems, The paper

3784

	describes how these techniques can be used to determine the feasibility

3785

	of expressions containing references to Ada arrays. Finally, we present

3786

	algorithms specific to generating test data under the modified condition

3787

	decision coverage (MCDC) criterion. While we realize that many of

3788

	the problems we are attempting to solve are, in general, undecidable,

3789

	we are encouraged by preliminary results obtained from running TSDT

3790

	against vendor supplied code. Based on our results, we feel these

3791

	techniques can be applied to a broad enough section of Ada code to

3792

	make them cost effective.},

3793

  citeulike-article-id = {2638010},

3794

  doi = {http://doi.acm.org/10.1145/186258.187150},

3795

  keywords = {bibtex-import, execution, generationsymbolic, infeasibility, problemtest,

3796

	vector},

3797

  local-url = {file://localhost/Users/michele/mogentes/bibliography/p95-jasper.pdf},

3798

  owner = {harald},

3799

  posted-at = {2008-04-07 16:23:44},

3800

  priority = {2},

3801

  timestamp = {2009.09.18},

3802

  url = {http://dx.doi.org/10.1145/186258.187150}

3803

3804

3805

@ARTICLE{Jia2010,

3806

  author = {Yue Jia and Mark Harman},

3807

  title = {An Analysis and Survey of the Development of Mutation Testing},

3808

  journal = {IEEE Transactions on Software Engineering},

3809

  year = {2010},

3810

  volume = {99},

3811

  number = {PrePrints},

3812

  address = {Los Alamitos, CA, USA},

3813

  doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2010.62},

3814

  issn = {0098-5589},

3815

  publisher = {IEEE Computer Society}

3816

3817

3818

@INPROCEEDINGS{Johnsen2004,

3819

  author = {Johnsen, Einar B. and Owe, Olaf },

3820

  title = {An Asynchronous Communication Model for Distributed Concurrent Objects},

3821

  booktitle = {SEFM '04: Proceedings of the Software Engineering and Formal Methods,

3822

	Second International Conference},

3823

  year = {2004},

3824

  pages = {188--197},

3825

  address = {Washington, DC, USA},

3826

  publisher = {IEEE Computer Society},

3827

  citeulike-article-id = {2653554},

3828

  doi = {http://dx.doi.org/10.1109/SEFM.2004.6},

3829

  owner = {harald},

3830

  posted-at = {2008-04-11 12:44:52},

3831

  priority = {3},

3832

  timestamp = {2009.09.18},

3833

  url = {http://dx.doi.org/10.1109/SEFM.2004.6}

3834

3835

3836

@BOOK{Jones1990,

3837

  title = {Systematic Software Development Using VDM},

3838

  publisher = {Prentice-Hall},

3839

  year = {1990},

3840

  author = {Cliff B. Jones},

3841

  series = {Series in Computer Science},

3842

  edition = {second},

3843

  owner = {harald},

3844

  timestamp = {2009.09.18}

3845

3846

3847

@BOOK{Jr.1999,

3848

  title = {Model Checking},

3849

  publisher = {The MIT Press},

3850

  year = {1999},

3851

  author = {Edmund M. Clarke Jr. and Orna Grumberg and Doron A. Peled},

3852

  isbn = {0262032708}

3853

3854

3855

@INPROCEEDINGS{Joebstl2010,

3856

  author = {Jöbstl, Elisabeth and Weiglhofer, Martin and Aichernig, Bernhard

3857

	K. and Wotawa, Franz},

3858

  title = {When {BDD}s Fail: Conformance Testing with Symbolic Execution and

3859

	{SMT} Solving},

3860

  booktitle = {Proceedings of the 2010 Third International Conference on Software

3861

	Testing, Verification and Validation},

3862

  year = {2010},

3863

  series = {ICST '10},

3864

  pages = {479--488},

3865

  address = {Washington, DC, USA},

3866

  publisher = {IEEE Computer Society},

3867

  acmid = {1828492},

3868

  doi = {http://dx.doi.org/10.1109/ICST.2010.48},

3869

  isbn = {978-0-7695-3990-4},

3870

  keywords = {model-based testing, symbolic execution, conformance testing, symbolic

3871

	input-output conformance, symbolic test case generation},

3872

  numpages = {10},

3873

  url = {http://dx.doi.org/10.1109/ICST.2010.48}

3874

3875

3876

@TECHREPORT{K.L.McMillan1992,

3877

  author = {{K.L. McMillan}},

3878

  title = {The {SMV} system},

3879

  institution = {Carnegie-Mellon University},

3880

  year = {1992},

3881

  number = {CMU-CS-92-131},

3882

  owner = {harald},

3883

  timestamp = {2009.09.18}

3884

3885

3886

@INPROCEEDINGS{Kansomkeat2003,

3887

  author = {Supaporn Kansomkeat and Wanchai Rivepiboon},

3888

  title = {Automated-generating test case using {UML} statechart diagrams},

3889

  booktitle = {Proc. of SAICSIT 2003},

3890

  year = {2003},

3891

  pages = {296--300}

3892

3893

3894

@INPROCEEDINGS{Khurshid2003,

3895

  author = {Khurshid, Sarfraz and Pasareanu, Corina S. and Visser, Willem },

3896

  title = {Generalized Symbolic Execution for Model Checking and Testing},

3897

  booktitle = {TACAS},

3898

  year = {2003},

3899

  pages = {553--568},

3900

  abstract = {Modern software systems, which often are concurrent and manipulate

3901

	complex data structures must be extremely reliable. We present a

3902

	novel framework based on symbolic execution, for automated checking

3903

	of such systems. We provide a two-fold generalization of traditional

3904

	symbolic execution based approaches. First, we define a source to

3905

	source translation to instrument a program, which enables standard

3906

	model checkers to perform symbolic execution of the program. Second,

3907

	we give a novel symbolic execution algorithm that handles dynamically

3908

	allocated structures (e.g., lists and trees), method preconditions

3909

	(e.g., acyclicity), data (e.g., integers and strings) and concurrency.

3910

	The program instrumentation enables a model checker to automatically

3911

	explore different program heap configurations and manipulate logical

3912

	formulae on program data (using a decision procedure). We illustrate

3913

	two applications of our framework: checking correctness of multi-threaded

3914

	programs that take inputs from unbounded domains with complex structure

3915

	and generation of non-isomorphic test inputs that satisfy a testing

3916

	criterion. Our implementation for Java uses the Java PathFinder model

3917

	checker.},

3918

  citeulike-article-id = {2638007},

3919

  keywords = {bibtex-import, bounding, executionloop, generationsymbolic, test,

3920

	vector},

3921

  local-url = {file://localhost/Users/michele/mogentes/bibliography/GSE.pdf},

3922

  owner = {harald},

3923

  posted-at = {2008-04-07 16:23:44},

3924

  priority = {2},

3925

  timestamp = {2009.09.18}

3926

3927

3928

@INPROCEEDINGS{Kicillof2007,

3929

  author = {Nicolas Kicillof and Wolfgang Grieskamp and Nikolai Tillmann and

3930

	Victor Braberman},

3931

  title = {Achieving both model and code coverage with automated gray-box testing},

3932

  booktitle = {A-MOST '07: Proceedings of the 3rd international workshop on Advances

3933

	in model-based testing},

3934

  year = {2007},

3935

  pages = {1--11},

3936

  address = {New York, NY, USA},

3937

  publisher = {ACM},

3938

  doi = {http://doi.acm.org/10.1145/1291535.1291536},

3939

  isbn = {978-1-59593-850-3},

3940

  location = {London, United Kingdom},

3941

  owner = {harald},

3942

  timestamp = {2009.09.18}

3943

3944

3945

@ARTICLE{King1976,

3946

  author = {King, James C. },

3947

  title = {Symbolic execution and program testing},

3948

  journal = {Commun. ACM},

3949

  year = {1976},

3950

  volume = {19},

3951

  pages = {385--394},

3952

  number = {7},

3953

  abstract = {This paper describes the symbolic execution of programs. Instead of

3954

	supplying the normal inputs to a program (e.g. numbers) one supplies

3955

	symbols representing arbitrary values. The execution proceeds as

3956

	in a normal execution except that values may he symbolic formulas

3957

	over the input symbols. The difficult, yet interesting issues arise

3958

	during the symbolic execution of conditional branch type statements.

3959

	A particular system called EFFIGY which provides symbolic execution

3960

	for program testing and debugging is also described, it interpretively

3961

	executes programs written in a simple PL/I style programming language.

3962

	It includes many standard debugging features, the ability to manage

3963

	and to prove things about symbolic expressions, a simple program

3964

	testing manager, and a program verifier. A brief discussion of the

3965

	relationship between symbolic execution and program proving is also

3966

	included.},

3967

  address = {New York, NY, USA},

3968

  citeulike-article-id = {2638012},

3969

  doi = {http://doi.acm.org/10.1145/360248.360252},

3970

  keywords = {bibtex-import, execution, generationsymbolic, test, vector},

3971

  local-url = {file://localhost/Users/michele/mogentes/bibliography/p385-king.pdf},

3972

  owner = {harald},

3973

  posted-at = {2008-04-07 16:23:45},

3974

  priority = {2},

3975

  publisher = {ACM},

3976

  timestamp = {2009.09.18},

3977

  url = {http://dx.doi.org/10.1145/360248.360252}

3978

3979

3980

@ARTICLE{Kleer1984,

3981

  author = {Johan De Kleer and John Seely Brown},

3982

  title = {A qualitative physics based on confluences},

3983

  journal = {Artif. Intell.},

3984

  year = {1984},

3985

  volume = {24},

3986

  pages = {7--83},

3987

  number = {1-3},

3988

  address = {Essex, UK},

3989

  doi = {http://dx.doi.org/10.1016/0004-3702(84)90037-7},

3990

  issn = {0004-3702},

3991

  owner = {harald},

3992

  publisher = {Elsevier Science Publishers Ltd.},

3993

  timestamp = {2009.09.18}

3994

3995

3996

@ARTICLE{Kozen1983,

3997

  author = {Dexter Kozen},

3998

  title = {Results on the Propositional mu-Calculus.},

3999

  journal = {Theor. Comput. Sci.},

4000

  year = {1983},

4001

  volume = {27},

4002

  pages = {333-354},

4003

  owner = {harald},

4004

  timestamp = {2009.09.18}

4005

4006

4007

@INPROCEEDINGS{Krenn2010,

4008

  author = {Willibald Krenn and Rupert Schlick and Bernhard K. Aichernig},

4009

  title = {Mapping {UML} to Labeled Transition Systems for Test-Case Generation

4010

	-- A Translation via Object-Oriented Action Systems},

4011

  booktitle = {Proc. of Formal Methods for Components and Objects (FMCO) 2009},

4012

  year = {2010},

4013

  volume = {6286},

4014

  series = {Lecture Notes in Computer Science},

4015

  publisher = {Springer},

4016

  owner = {wkrenn},

4017

  timestamp = {2010.03.18}

4018

4019

4020

@ARTICLE{Krichen2009,

4021

  author = {Krichen, Moez and Tripakis, Stavros},

4022

  title = {Conformance testing for real-time systems},

4023

  journal = {Form. Methods Syst. Des.},

4024

  year = {2009},

4025

  volume = {34},

4026

  pages = {238--304},

4027

  number = {3},

4028

  address = {Hingham, MA, USA},

4029

  doi = {http://dx.doi.org/10.1007/s10703-009-0065-1},

4030

  issn = {0925-9856},

4031

  publisher = {Kluwer Academic Publishers}

4032

4033

4034

@BOOK{Kuipers1994,

4035

  title = {Qualitative Reasoning: Modeling and Simulation with Incomplete Knowledge},

4036

  publisher = {MIT Press},

4037

  year = {1994},

4038

  author = {Kuipers, Benjamin},

4039

  keywords = {QSIM},

4040

  owner = {harald},

4041

  priority = {0},

4042

  timestamp = {2009.09.18}

4043

4044

4045

@INPROCEEDINGS{Larsen2005a,

4046

  author = {Kim G. Larsen and Marius Mikucionis and Brian Nielsen},

4047

  title = {Online Testing of Real-Time Systems Using UPPAAL: Status and Future

4048

	Work},

4049

  booktitle = {Perspectives of Model-Based Testing},

4050

  year = {2005},

4051

  editor = {Ed Brinksma and Wolfgang Grieskamp and Jan Tretmans},

4052

  number = {04371},

4053

  series = {Dagstuhl Seminar Proceedings},

4054

  publisher = {Internationales Begegnungs- und Forschungszentrum fuer Informatik

4055

	(IBFI), Schloss Dagstuhl, Germany},

4056

  note = {$<$http://drops.dagstuhl.de/opus/volltexte/2005/326$>$ [date of citation:

4057

	2005-01-01]},

4058

  issn = {1862-4405},

4059

  optaddress = {Dagstuhl, Germany},

4060

  optannote = {Keywords: Online testing, black-box testing, real-time systems, embedded

4061

	systems, symbolic state representation, relativized timed input/output

4062

	conformance, mo},

4063

  opturl = {http://drops.dagstuhl.de/opus/volltexte/2005/326 [date of citation:

4064

	2005-01-01]},

4065

  owner = {harald},

4066

  timestamp = {2009.09.18}

4067

4068

4069

@INPROCEEDINGS{Larsen2005,

4070

  author = {Kim G. Larsen and Marius Mikucionis and Brian Nielsen and Arne Skou},

4071

  title = {Testing real-time embedded software using UPPAAL-TRON: an industrial

4072

	case study},

4073

  booktitle = {EMSOFT '05: Proceedings of the 5th ACM international conference on

4074

	Embedded software},

4075

  year = {2005},

4076

  pages = {299--306},

4077

  address = {New York, NY, USA},

4078

  publisher = {ACM},

4079

  doi = {http://doi.acm.org/10.1145/1086228.1086283},

4080

  isbn = {1-59593-091-4},

4081

  location = {Jersey City, NJ, USA},

4082

  owner = {harald},

4083

  timestamp = {2009.09.18}

4084

4085

4086

@INPROCEEDINGS{LaValle1999,

4087

  author = {Steven M. LaValle and James J. Kuffner Jr.},

4088

  title = {Randomized Kinodynamic Planning},

4089

  booktitle = {International Conference on Robotics and Automation},

4090

  year = {1999},

4091

  pages = {473-479},

4092

  owner = {harald},

4093

  timestamp = {2009.09.18}

4094

4095

4096

@INCOLLECTION{Leavens1999,

4097

  author = {Gary T. Leavens and Albert L. Baker and Clyde Ruby},

4098

  title = {{JML}: {A} Notation for Detailed Design},

4099

  booktitle = {Behavioral Specifications of Businesses and Systems},

4100

  publisher = {Kluwer Academic Publishers},

4101

  year = {1999},

4102

  editor = {Haim Kilov and Bernhard Rumpe and Ian Simmonds},

4103

  pages = {175--188},

4104

  owner = {harald},

4105

  timestamp = {2009.09.18},

4106

  url = {citeseer.ist.psu.edu/leavens99jml.html}

4107

4108

4109

@ARTICLE{Lee1996,

4110

  author = {David Lee and Mihakus Yannakakis},

4111

  title = {Principles and Methods of Testing Finite State Machines -- A Survey},

4112

  journal = {Proceedings of the IEEE},

4113

  year = {1996},

4114

  volume = {84},

4115

  pages = {1090--1123},

4116

  number = {8},

4117

  month = {August},

4118

  abstract = {This paper reviews possible test generation techniques on finite state

4119

	machines. It discusses distinquishing sequences, seperating sequences,

4120

	intput/output sequences, seperating sequences and so on. It concludes

4121

	with a short view on other state machine representations such as

4122

	extended finite state machines and probabilistic state machines.},

4123

  file = {lee1996principles.pdf:lee1996principles.pdf:PDF},

4124

  filename = {./test\_generation/lee96principles.pdf},

4125

  keywords = {Testing, FSM, EFSM, PFSM, NFSM},

4126

  owner = {harald},

4127

  timestamp = {2009.09.18}

4128

4129

4130

@ARTICLE{Lefebvre2006,

4131

  author = {Marie-Anne Lefebvre and Hervé Guéguen},

4132

  title = {Hybrid abstractions of affine systems},

4133

  journal = {Nonlinear Analysis},

4134

  year = {2006},

4135

  volume = {65},

4136

  pages = {1150 - 1167},

4137

  number = {6},

4138

  note = {Hybrid Systems and Applications (5)},

4139

  doi = {DOI: 10.1016/j.na.2005.12.016},

4140

  issn = {0362-546X},

4141

  keywords = {Hybrid systems},

4142

  url = {http://www.sciencedirect.com/science/article/B6V0Y-4JFGF71-2/2/9f7f4ee86fb16bf7f463a65950bc6feb}

4143

4144

4145

@INPROCEEDINGS{Legeard2002,

4146

  author = {Bruno Legeard and Fabien Peureux and Mark Utting},

4147

  title = {Automated Boundary Testing from {Z} and {B}},

4148

  booktitle = {Proceedings of FME 2002: Formal Methods --- Getting IT Right, International

4149

	Symposium of Formal Methods Europe, July 2002, Copenhagen, Denmark},

4150

  year = {2002},

4151

  editor = {Lars-Henrik Eriksson and Peter A. Lindsay},

4152

  volume = {2391},

4153

  series = {Lecture Notes in Computer Science},

4154

  pages = {21--40},

4155

  publisher = {Springer-Verlag},

4156

  owner = {harald},

4157

  timestamp = {2009.09.18}

4158

4159

4160

@ARTICLE{Leveson2004,

4161

  author = {Nancy G. Leveson},

4162

  title = {The role of software in spacecraft accidents},

4163

  journal = {AIAA Journal of Spacecraft and Rockets},

4164

  year = {2004},

4165

  volume = {41},

4166

  pages = {564--575}

4167

4168

4169

@INPROCEEDINGS{Ma2006,

4170

  author = {Ma, Yu-Seung and Offutt, Jeff and Kwon, Yong-Rae},

4171

  title = {MuJava: a mutation system for java},

4172

  booktitle = {ICSE '06: Proceedings of the 28th international conference on Software

4173

	engineering},

4174

  year = {2006},

4175

  pages = {827--830},

4176

  address = {New York, NY, USA},

4177

  publisher = {ACM},

4178

  bdsk-url-1 = {http://doi.acm.org/10.1145/1134285.1134425},

4179

  doi = {http://doi.acm.org/10.1145/1134285.1134425},

4180

  isbn = {1-59593-375-1},

4181

  location = {Shanghai, China}

4182

4183

4184

@INPROCEEDINGS{Maibaum2003,

4185

  author = {Tom Maibaum},

4186

  title = {In Memoriam {Armando Mart\'{i}n Haeberer}},

4187

  booktitle = {Formal Methods at the Crossroads: from Panacea to Foundational Support},

4188

  year = {2003},

4189

  editor = {Bernhard K.\ Aichernig and Tom Maibaum},

4190

  volume = {2757},

4191

  series = {Lecture Notes in Computer Science},

4192

  pages = {1--25},

4193

  publisher = {Springer-Verlag},

4194

  owner = {harald},

4195

  timestamp = {2009.09.18}

4196

4197

4198

@PHDTHESIS{Man2006,

4199

  author = {K.L. Man and R.R.H. Schiffelers},

4200

  title = {Formal Specification and Analysis of Hybrid Systems},

4201

  school = {Eindhoven University of Technology},

4202

  year = {2006},

4203

  owner = {harald},

4204

  timestamp = {2009.09.18}

4205

4206

4207

@BOOK{Matiyasevich1993,

4208

  title = {Hilbert's tenth problem},

4209

  publisher = {MIT Press},

4210

  year = {1993},

4211

  author = {Matiyasevich, Yuri V.},

4212

  address = {Cambridge, MA, USA},

4213

  isbn = {0-262-13295-8}

4214

4215

4216

@BOOK{McMillan1993,

4217

  title = {Symbolic Model Checking},

4218

  publisher = {Kluwer Academic Publishers},

4219

  year = {1993},

4220

  author = {Kenneth L. McMillan},

4221

  address = {Norwell, MA, USA},

4222

  isbn = {0792393805},

4223

  owner = {harald},

4224

  timestamp = {2009.09.18}

4225

4226

4227

@ARTICLE{Memon2007,

4228

  author = {Atif M. Memon},

4229

  title = {An event-flow model of GUI-based applications for testing},

4230

  journal = {Softw. Test., Verif. Reliab.},

4231

  year = {2007},

4232

  volume = {17},

4233

  pages = {137-157},

4234

  number = {3},

4235

  bibsource = {DBLP, http://dblp.uni-trier.de},

4236

  ee = {http://dx.doi.org/10.1002/stvr.364},

4237

  owner = {harald},

4238

  timestamp = {2009.09.18}

4239

4240

4241

@BOOK{Meyer1997,

4242

  title = {Object-Oriented Software Construction},

4243

  publisher = {Prentice Hall Professional Technical Reference},

4244

  year = {1997},

4245

  author = {Bertrand Meyer},

4246

  abstract = {The developer of the acclaimed Eiffel programming language comes through

4247

	with one of the clearest and most informative books about computers

4248

	ever committed to paper. <i>Object-Oriented Software Construction</i>

4249

	is the gospel of object-oriented technology and it deserves to be

4250

	spread everywhere. Meyer opens with coverage of the need for an object-oriented

4251

	approach to software development, citing improved quality and development

4252

	speed as key advantages of the approach. He then explains all the

4253

	key criteria that define an object- oriented approach to a problem.

4254

	Meyer pays attention to techniques, such as classes, objects, memory

4255

	management, and more, returning to each technique and polishing his

4256

	readers' knowledge of it as he explains how to employ it "well."

4257

	In a section on advanced topics, Meyer explores interesting and relevant

4258

	topics, such as persistent objects stored in a database. He also

4259

	offers a sort of "Do and Don't" section in which he enumerates common

4260

	mistakes and ways to avoid them. Management information isn't the

4261

	main point of <i>Object-Oriented Software Construction</i>, but you'll

4262

	find some in its pages. Meyer concludes his tour de force with comparisons

4263

	of all the key object-oriented languages, including Java. He also

4264

	covers the potential of simulating object technology in non-object-oriented

4265

	languages, such as Pascal and Fortran. The companion CD-ROM includes

4266

	the full text of this book in hypertext form, as well as some tools

4267

	for designing object-oriented systems. If you program computers,

4268

	you need to read this book. <I>Recipient of the 1997 Jolt Award.</I>

4269

	<P>The developer of the acclaimed Eiffel programming language comes

4270

	through with one of the clearest and most informative books about

4271

	computers ever committed to paper. Object-Oriented Software Construction

4272

	is the gospel of object-oriented technology and it deserves to be

4273

	spread everywhere. Meyer opens with coverage of the need for an object-oriented

4274

	approach to software development, citing improved quality and development

4275

	speed as key advantages of the approach. He then explains all the

4276

	key criteria that define an object- oriented approach to a problem.

4277

	Meyer pays attention to techniques, such as classes, objects, memory

4278

	management, and more, returning to each technique and polishing his

4279

	readers' knowledge of it as he explains how to employ it "well."

4280

	In a section on advanced topics, Meyer explores interesting and relevant

4281

	topics, such as persistent objects stored in a database. He also

4282

	offers a sort of "Do and Don't" section in which he enumerates common

4283

	mistakes and ways to avoid them. Management information isn't the

4284

	main point of Object-Oriented Software Construction, but you'll find

4285

	some in its pages. Meyer concludes his tour de force with comparisons

4286

	of all the key object-oriented languages, including Java. He also

4287

	covers the potential of simulating object technology in non-object-oriented

4288

	languages, such as Pascal and Fortran. The companion CD-ROM includes

4289

	the full text of this book in hypertext form, as well as some tools

4290

	for designing object-oriented systems. If you program computers,

4291

	you need to read this book.},

4292

  isbn = {0-13-629155-4},

4293

  owner = {harald},

4294

  timestamp = {2009.09.18}

4295

4296

4297

@BOOK{Milner1999,

4298

  title = {Communicating and Mobile Systems: the Pi-Calculus},

4299

  publisher = {{Cambridge University Press}},

4300

  year = {1999},

4301

  author = {Milner, Robin },

4302

  month = {June},

4303

  citeulike-article-id = {500640},

4304

  howpublished = {Paperback},

4305

  isbn = {0521658691},

4306

  keywords = {calculus, process},

4307

  owner = {harald},

4308

  priority = {3},

4309

  timestamp = {2009.09.18},

4310

  url = {http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20\&amp;path=ASIN/0521658691}

4311

4312

4313

@BOOK{Milner1982,

4314

  title = {{A Calculus of Communicating Systems}},

4315

  publisher = {Springer-Verlag New York, Inc. Secaucus, NJ, USA},

4316

  year = {1982},

4317

  author = {Milner, R.},

4318

  owner = {harald},

4319

  timestamp = {2009.09.18}

4320

4321

4322

@BOOK{Morgan1990,

4323

  title = {Programming from Specifications},

4324

  publisher = {Prentice-Hall International},

4325

  year = {1990},

4326

  author = {Carroll C.\ Morgan},

4327

  series = {Series in Computer Science},

4328

  owner = {harald},

4329

  timestamp = {2009.09.18}

4330

4331

4332

@INPROCEEDINGS{Mosses1999,

4333

  author = {Peter D.~Mosses},

4334

  title = {{CASL}: A guided tour of its design},

4335

  booktitle = {Proceedings of WADT'98},

4336

  year = {1999},

4337

  volume = {1589},

4338

  series = {Lecture Notes in Computer Science},

4339

  pages = {216--240},

4340

  publisher = {Springer-Verlag},

4341

  owner = {harald},

4342

  timestamp = {2009.09.18}

4343

4344

4345

@INPROCEEDINGS{Moura2004,

4346

  author = {Leonardo de Moura and Sam Owre and Harald Rue{\ss} and John Rushbyand

4347

	N. Shankar and Maria Sorea and Ashish Tiwari},

4348

  title = {{SAL 2}},

4349

  booktitle = {Computer-Aided Verification, {CAV} 2004},

4350

  year = {2004},

4351

  editor = {Rajeev Alur and Doron Peled},

4352

  volume = {3114},

4353

  series = {Lecture Notes in Computer Science},

4354

  pages = {496--500},

4355

  address = {Boston, MA},

4356

  month = jul,

4357

  publisher = {Springer-Verlag},

4358

  owner = {harald},

4359

  timestamp = {2009.09.18}

4360

4361

4362

@BOOK{Myers2004,

4363

  title = {{The Art of Software Testing}},

4364

  publisher = {Wiley},

4365

  year = {2004},

4366

  author = {Myers, G. J. },

4367

  citeulike-article-id = {2804765},

4368

  keywords = {fundamentals},

4369

  owner = {harald},

4370

  posted-at = {2008-05-16 10:32:55},

4371

  priority = {4},

4372

  timestamp = {2009.09.18}

4373

4374

4375

@BOOK{Myers2004a,

4376

  title = {The Art of Software Testing},

4377

  publisher = {John Wiley \& Sons},

4378

  year = {2004},

4379

  author = {Myers, Glenford J. and Sandler, Corey},

4380

  isbn = {0471469122}

4381

4382

4383

@INPROCEEDINGS{Nahhal2007,

4384

  author = {Tarik Nahhal and Thao Dang},

4385

  title = {Test Coverage for Continuous and Hybrid Systems},

4386

  booktitle = {Computer Aided Verification},

4387

  year = {2007},

4388

  pages = {449-462},

4389

  doi = {http://dx.doi.org/10.1007/978-3-540-73368-3_47},

4390

  owner = {harald},

4391

  timestamp = {2009.09.18}

4392

4393

4394

@INPROCEEDINGS{Nicola1990,

4395

  author = {Rocco De Nicola and Frits Vaandrager},

4396

  title = {Action versus state based logics for transition systems},

4397

  booktitle = {Proceedings of the LITP spring school on theoretical computer science

4398

	on Semantics of systems of concurrent processes},

4399

  year = {1990},

4400

  pages = {407--419},

4401

  address = {New York, NY, USA},

4402

  publisher = {Springer-Verlag New York, Inc.},

4403

  isbn = {0-387-53479-2},

4404

  location = {La Roche Posay, France},

4405

  owner = {harald},

4406

  timestamp = {2009.09.18}

4407

4408

4409

@BOOK{Nipkow2002,

4410

  title = {Isabelle/HOL - A Proof Assistant for Higher-Order Logic},

4411

  publisher = {Springer},

4412

  year = {2002},

4413

  author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},

4414

  volume = {2283},

4415

  series = {Lecture Notes in Computer Science},

4416

  bibsource = {DBLP, http://dblp.uni-trier.de},

4417

  isbn = {3-540-43376-7},

4418

  owner = {harald},

4419

  timestamp = {2009.09.18}

4420

4421

4422

@INPROCEEDINGS{Offutt1996,

4423

  author = {Offutt, A.J. and Jie Pan},

4424

  title = {Detecting equivalent mutants and the feasible path problem},

4425

  year = {1996},

4426

  pages = {224 -236},

4427

  month = {jun.},

4428

  doi = {10.1109/CMPASS.1996.507890},

4429

  journal = {Computer Assurance, 1996. COMPASS '96, 'Systems Integrity. Software

4430

	Safety. Process Security'. Proceedings of the Eleventh Annual Conference

4431

	on},

4432

  keywords = {critical software;equivalent mutant programs;feasible path problem;high

4433

	reliability;infeasible constraints;mathematical constraint systems;mathematical

4434

	constraints;mutation testing;proof of concept implementation;software

4435

	unit testing;test criteria;program testing;safety-critical software;software

4436

	quality;}

4437

4438

4439

@ARTICLE{Offutt1997,

4440

  author = {A. Jefferson Offutt and Jie Pan},

4441

  title = {Automatically Detecting Equivalent Mutants and Infeasible Paths},

4442

  journal = {Software Testing, Veri and Reliability},

4443

  year = {1997},

4444

  volume = {7},

4445

  pages = {165--192}

4446

4447

4448

@ARTICLE{Oliveira2007,

4449

  author = {Marcel Oliveira and Ana Cavalcanti and Jim Woodcock},

4450

  title = {A Denotational Semantics for Circus},

4451

  journal = {Electr. Notes Theor. Comput. Sci.},

4452

  year = {2007},

4453

  volume = {187},

4454

  pages = {107-123},

4455

  bibsource = {DBLP, http://dblp.uni-trier.de},

4456

  ee = {http://dx.doi.org/10.1016/j.entcs.2006.08.047},

4457

  owner = {harald},

4458

  timestamp = {2009.09.18}

4459

4460

4461

@PHDTHESIS{Oster2007,

4462

  author = {Norbert Oster},

4463

  title = {Automatische Generierung optimaler struktureller Testdaten f{\"u}r

4464

	objekt-orientierte Software mittels multi-objektiver Metaheuristiken

4465

},

4466

  school = {Friedrich--Alexander University, Erlangen-N{\"u}rnberg},

4467

  year = {2007},

4468

  owner = {harald},

4469

  timestamp = {2009.09.18}

4470

4471

4472

@ARTICLE{Ostrand1998,

4473

  author = {Thomas Ostrand and Aaron Anodide and Herbert Foster and Tarak Goradia},

4474

  title = {A visual test development environment for GUI systems},

4475

  journal = {SIGSOFT Softw. Eng. Notes},

4476

  year = {1998},

4477

  volume = {23},

4478

  pages = {82--92},

4479

  number = {2},

4480

  address = {New York, NY, USA},

4481

  doi = {http://doi.acm.org/10.1145/271775.271793},

4482

  issn = {0163-5948},

4483

  owner = {harald},

4484

  publisher = {ACM},

4485

  timestamp = {2009.09.18}

4486

4487

4488

@ARTICLE{Ostrand1988,

4489

  author = {T. J. Ostrand and M. J. Balcer},

4490

  title = {The category-partition method for specifying and generating fuctional

4491

	tests},

4492

  journal = {Commun. ACM},

4493

  year = {1988},

4494

  volume = {31},

4495

  pages = {676--686},

4496

  number = {6},

4497

  address = {New York, NY, USA},

4498

  doi = {http://doi.acm.org/10.1145/62959.62964},

4499

  issn = {0001-0782},

4500

  owner = {harald},

4501

  publisher = {ACM},

4502

  timestamp = {2009.09.18}

4503

4504

4505

@INPROCEEDINGS{Paradkar2005,

4506

  author = {Paradkar, Amit },

4507

  title = {Case studies on fault detection effectiveness of model based test

4508

	generation techniques},

4509

  booktitle = {A-MOST '05: Proceedings of the 1st international workshop on Advances

4510

	in model-based testing},

4511

  year = {2005},

4512

  pages = {1--7},

4513

  address = {New York, NY, USA},

4514

  publisher = {ACM},

4515

  abstract = {Model-based test generation (MBTG) is becoming an area of active research.

4516

	These techniques differ in terms of (1) modeling notations used,

4517

	and (2) the adequacy criteria used for test generation. This paper

4518

	(1) reviews different classes of MBTG techniques at a conceptual

4519

	level, and (2) reports results of two case studies comparing various

4520

	techniques in terms of their fault detection effectiveness. Our results

4521

	indicate that MBTG technique which employs mutation and explicitly

4522

	generates state verification sequences has better fault detection

4523

	effectiveness than those based on boundary values, and predicate

4524

	coverage criteria for transitions. Instead of a default adequacy

4525

	criteria, certain techniques allow the user to specify test objectives

4526

	in addition to the model. Our experience indicates that the task

4527

	of defining appropriate test objectives is not intuitive. Furthermore,

4528

	notations provided to describe such test objectives may have inadequate

4529

	expressive power. We posit the need for a suitable fault modeling

4530

	notation.},

4531

  citeulike-article-id = {2638015},

4532

  doi = {http://doi.acm.org/10.1145/1083274.1083286},

4533

  keywords = {bibtex-import},

4534

  local-url = {file://localhost/Users/michele/mogentes/bibliography/p12-paradkar.pdf},

4535

  owner = {harald},

4536

  posted-at = {2008-04-07 16:23:45},

4537

  priority = {2},

4538

  timestamp = {2009.09.18},

4539

  url = {http://doi.acm.org/10.1145/1083274.1083286}

4540

4541

4542

@TECHREPORT{Paul2007,

4543

  author = {Paul},

4544

  title = {Testing with model checkers: A survey},

4545

  institution = {Competence Network Softnet Austria},

4546

  year = {2007},

4547

  number = {SNA-TR-2007-P2-04},

4548

  citeulike-article-id = {2637994},

4549

  keywords = {bibtex-import, tug},

4550

  local-url = {file://localhost/Users/michele/mogentes/bibliography/SNA-TR-2007-P2-04.pdf},

4551

  owner = {harald},

4552

  posted-at = {2008-04-07 16:23:41},

4553

  priority = {2},

4554

  timestamp = {2009.09.18}

4555

4556

4557

@INPROCEEDINGS{Peischl2007,

4558

  author = {Peischl, Bernhard and Weiglhofer, Martin and Wotawa, Franz },

4559

  title = {Executing Abstract Test Cases},

4560

  booktitle = {In Proceedings of the Model-based Testing Workshop held in conjunction

4561

	with the 37th Annual Congress of the Gesellschaft fuer Informatik

4562

	(MOTES 2007)},

4563

  year = {2007},

4564

  pages = {421--426},

4565

  month = {September},

4566

  abstract = {This paper shows how to use an on-the-fly verification algo rithm,

4567

	that verifies the equivalence of labeled transition sys tems, for

4568

	the verification of the input output conformance (ioco) of input

4569

	output labeled transition systems. Since ioco is usually used for

4570

	testing there are several requirements on the input output labeled

4571

	transition system (IOLTS) that are used for test generation. We show

4572

	how to take care of these requirements during the on-the-fly verification.

4573

	Thus the presented approach can be applied to IOLTSs that do not

4574

	initially fulfill these requirements. Finally, we discuss the evaluation

4575

	of a prototype implementation on the datalink protocol.},

4576

  citeulike-article-id = {2637992},

4577

  keywords = {bibtex-import, tug},

4578

  local-url = {file://localhost/Users/michele/mogentes/bibliography/motes2007.pdf},

4579

  owner = {harald},

4580

  posted-at = {2008-04-07 16:23:41},

4581

  priority = {2},

4582

  timestamp = {2009.09.18}

4583

4584

4585

@INBOOK{Peled2003,

4586

  title = {Model Checking and Testing Combined},

4587

  publisher = {Springer Berlin / Heidelberg},

4588

  year = {2003},

4589

  author = {Peled, Doron },

4590

  volume = {2719/2003},

4591

  series = {Lecture Notes in Computer Science},

4592

  month = {jan},

4593

  abstract = {Model checking is a technique for automatically checking properties

4594

	of models of systems. We present here several combinations of model

4595

	checking with testing techniques. This allows checking systems when

4596

	no model is given, when the model is inaccurate, or when only a part

4597

	of its description is given.},

4598

  citeulike-article-id = {2638004},

4599

  doi = {10.1007/3-540-45061-0\_5},

4600

  keywords = {bibtex-import, black-box, testing},

4601

  local-url = {file://localhost/Users/michele/mogentes/bibliography/peled-modcheckandtest.pdf},

4602

  owner = {harald},

4603

  posted-at = {2008-04-07 16:23:44},

4604

  priority = {2},

4605

  timestamp = {2009.09.18},

4606

  url = {http://dx.doi.org/10.1007/3-540-45061-0\_5}

4607

4608

4609

@INPROCEEDINGS{Peleska1996,

4610

  author = {Jan Peleska and Michael Siegel},

4611

  title = {From Testing Theory to Test Driver Implementation},

4612

  booktitle = {FME'96: Industrial Benefit and Advances in Formal Methods},

4613

  year = {1996},

4614

  editor = {Marie-Claude Gaudel and Jim Woodcock},

4615

  pages = {538--556},

4616

  month = {March},

4617

  publisher = {Springer-Verlag},

4618

  key = {Peleska\&96},

4619

  libnum = {6},

4620

  owner = {harald},

4621

  timestamp = {2009.09.18}

4622

4623

4624

@INPROCEEDINGS{Petrenko2002,

4625

  author = {Alexandre Petrenko and Nina Yevtushenko},

4626

  title = {Queued Testing of Transition Systems with Inputs and Outputs},

4627

  booktitle = {Proceedings of the Workshop on Formal Approaches to Testing Of Software

4628

	(Fates'02), A Satellite Workshop of Concur'02},

4629

  year = {2002},

4630

  editor = {Rob Hierons and Thierry J\'{e}ron},

4631

  pages = {79--94},

4632

  address = {Brno, Czech Republic},

4633

  month = {August},

4634

  owner = {harald},

4635

  timestamp = {2009.09.18}

4636

4637

4638

@ARTICLE{Platzer2008,

4639

  author = {Andr{\'e} Platzer},

4640

  title = {Differential Dynamic Logic for Hybrid Systems.},

4641

  journal = {Journal of Automated Reasoning},

4642

  year = {2008},

4643

  volume = {41},

4644

  pages = {143-189},

4645

  number = {2},

4646

  abstract = { Hybrid systems are models for complex physical systems and are defined

4647

	as dynamical systems with interacting discrete transitions and continuous

4648

	evolutions along differential equations. With the goal of developing

4649

	a theoretical and practical foundation for deductive verification

4650

	of hybrid systems, we introduce a dynamic logic for hybrid programs,

4651

	which is a program notation for hybrid systems. As a verification

4652

	technique that is suitable for automation, we introduce a free variable

4653

	proof calculus with a novel combination of real-valued free variables

4654

	and Skolemisation for lifting quantifier elimination for real arithmetic

4655

	to dynamic logic. The calculus is compositional, i.e., it reduces

4656

	properties of hybrid programs to properties of their parts. Our main

4657

	result proves that this calculus axiomatises the transition behaviour

4658

	of hybrid systems completely relative to differential equations.

4659

	In a case study with cooperating traffic agents of the European Train

4660

	Control System, we further show that our calculus is well-suited

4661

	for verifying realistic hybrid systems with parametric system dynamics.

4662

},

4663

  doi = {10.1007/s10817-008-9103-8},

4664

  issn = {0168-7433},

4665

  keywords = {dynamic logic, differential equations, sequent calculus, axiomatisation,

4666

	automated theorem proving, verification of hybrid systems},

4667

  longjournal = {Journal of Automated Reasoning},

4668

  medjournal = {J. Autom. Reasoning}

4669

4670

4671

@INCOLLECTION{Platzer2008a,

4672

  author = {Platzer, André and Quesel, Jan-David},

4673

  title = {KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)},

4674

  booktitle = {Automated Reasoning},

4675

  publisher = {Springer Berlin, Heidelberg},

4676

  year = {2008},

4677

  editor = {Armando, Alessandro and Baumgartner, Peter and Dowek, Gilles},

4678

  volume = {5195},

4679

  series = {Lecture Notes in Computer Science},

4680

  pages = {171-178}

4681

4682

4683

@INPROCEEDINGS{Platzer2008b,

4684

  author = {Platzer, Andr\'{e} and Quesel, Jan-David},

4685

  title = {Logical Verification and Systematic Parametric Analysis in Train

4686

	Control},

4687

  booktitle = {HSCC '08: Proceedings of the 11th international workshop on Hybrid

4688

	Systems},

4689

  year = {2008},

4690

  pages = {646--649},

4691

  address = {Berlin, Heidelberg},

4692

  publisher = {Springer-Verlag},

4693

  doi = {http://dx.doi.org/10.1007/978-3-540-78929-1_55},

4694

  isbn = {978-3-540-78928-4},

4695

  location = {St. Louis, MO, USA}

4696

4697

4698

@INPROCEEDINGS{Pnueli1977,

4699

  author = {Amir Pnueli},

4700

  title = {The Temporal Logic of Programs},

4701

  booktitle = {18th Annual Symposium on Foundations of Computer Science, 31 October-2

4702

	November, Providence, Rhode Island, USA},

4703

  year = {1977},

4704

  pages = {46--57},

4705

  publisher = {IEEE},

4706

  bibsource = {DBLP, http://dblp.uni-trier.de},

4707

  owner = {harald},

4708

  timestamp = {2009.09.18}

4709

4710

4711

@ARTICLE{Ronkko2003,

4712

  author = {Mauno R\"{o}nkk\"{o} and Anders P. Ravn and Kaisa Sere},

4713

  title = {Hybrid action systems},

4714

  journal = {Theor. Comput. Sci.},

4715

  year = {2003},

4716

  volume = {290},

4717

  pages = {937--973},

4718

  number = {1},

4719

  address = {Essex, UK},

4720

  doi = {http://dx.doi.org/10.1016/S0304-3975(02)00547-9},

4721

  issn = {0304-3975},

4722

  owner = {harald},

4723

  publisher = {Elsevier Science Publishers Ltd.},

4724

  timestamp = {2009.09.18}

4725

4726

4727

@INPROCEEDINGS{Ronkko1999,

4728

  author = {R\"{o}nkk\"{o},, Mauno and Sere,, Kaisa},

4729

  title = {Refinement and Continuous Behaviour},

4730

  booktitle = {HSCC '99: Proceedings of the Second International Workshop on Hybrid

4731

	Systems},

4732

  year = {1999},

4733

  pages = {223--237},

4734

  address = {London, UK},

4735

  publisher = {Springer-Verlag},

4736

  isbn = {3-540-65734-7}

4737

4738

4739

@BOOK{RAISELanguageGroup1995,

4740

  title = {The {RAISE} Development Method},

4741

  publisher = {Prentice Hall},

4742

  year = {1995},

4743

  author = {{RAISE Language Group}, The},

4744

  series = {BCS Practitioner Series},

4745

  annote = {\CRCS{D.2.1, 000427}},

4746

  owner = {harald},

4747

  timestamp = {2009.09.18}

4748

4749

4750

@ARTICLE{RamamoorthyDec.1976,

4751

  author = {Ramamoorthy, C. V. and Ho and Chen, W. T. },

4752

  title = {On the Automated Generation of Program Test Data},

4753

  journal = {Software Engineering, Transactions on},

4754

  year = {Dec. 1976},

4755

  volume = {SE-2},

4756

  pages = {293--300},

4757

  number = {4},

4758

  abstract = {Software validation through testing will continue to be a very important

4759

	tool for ensuring correctness of large scale software systems. Automation

4760

	of testing tools can greatly enhance their power and reduce testing

4761

	cost. In,this paper, techniques for automated test data generation

4762

	are discussed. Given a program graph, a set of paths are identified

4763

	to satisfy some given testing criteria. When a path or a program

4764

	segment is specified, symbolic execution is used for generating input

4765

	constraints which defme a set of inputs for executing this path or

4766

	segment. Problems encountered in symbolic execution are discussed.

4767

	A new approach for resolving array reference ambiguities and a procedure

4768

	for generating test inputs satisfying input constraints are proposed.

4769

	References to arrays are recorded in a table during symbolic execution

4770

	and ambiguities are resolved when test data are-generated to evaluate

4771

	the subscript expressions. The implementation of a test data generator

4772

	for Fortran programs incorporating these techniques is also described.},

4773

  citeulike-article-id = {2638011},

4774

  keywords = {ambiguity, array, bibtex-import, constraint, execution, generation,

4775

	path, reference, solver, symbolic, test, vector},

4776

  local-url = {file://localhost/Users/michele/mogentes/bibliography/01702386.pdf},

4777

  owner = {harald},

4778

  posted-at = {2008-04-07 16:23:45},

4779

  priority = {2},

4780

  timestamp = {2009.09.18}

4781

4782

4783

@ARTICLE{Rapps1985,

4784

  author = {Sandra Rapps and Elaine J. Weyuker},

4785

  title = {Selecting Software Test Data Using Data Flow Information},

4786

  journal = {IEEE Trans. Software Eng.},

4787

  year = {1985},

4788

  volume = {11},

4789

  pages = {367-375},

4790

  number = {4},

4791

  bibsource = {DBLP, http://dblp.uni-trier.de},

4792

  owner = {harald},

4793

  timestamp = {2009.09.18}

4794

4795

4796

@TECHREPORT{ReactiveSystems2003,

4797

  author = {{Reactive Systems}},

4798

  title = {Model-Based Testing and Validation with {Reactis}},

4799

  institution = {Reactive Systems, Inc.},

4800

  year = {2003},

4801

  key = {{Reactive Systems, Inc.}},

4802

  owner = {harald},

4803

  timestamp = {2009.09.18}

4804

4805

4806

@ARTICLE{Richters1998,

4807

  author = {Richters, Mark and Gogolla, Martin},

4808

  title = {On Formalizing the UML Object Constraint Language OCL},

4809

  journal = {Conceptual Modeling --ER '98},

4810

  year = {1998},

4811

  pages = {449--464},

4812

  abstract = {We present a formal semantics for the Object Constraint Language (OCL)

4813

	which is part of the Unified Modeling Language (UML) - an emerging

4814

	standard language and notation for object-oriented analysis and design.

4815

	In context of information systems modeling, UML class diagrams can

4816

	be utilized for describing the overall structure, whereas additional

4817

	integrity constraints and queries are specified with OCL expressions.

4818

	By using OCL, constraints and queries can be specified in a formal

4819

	yet comprehensible way. However, the OCL itself is currently defined

4820

	only in a semi-formal way. Thus the semantics of constraints is in

4821

	general not precisely defined. Our approach gives precise meaning

4822

	to OCL concepts and to some central aspects of UML class models.

4823

	A formal semantics facilitates verification, validation and simulation

4824

	of models and helps to improve the quality of models and software

4825

	designs.},

4826

  date-added = {2008-05-27 02:43:14 +0200},

4827

  date-modified = {2008-05-27 02:43:14 +0200},

4828

  owner = {harald},

4829

  timestamp = {2009.09.18},

4830

  ty = {CHAPTER},

4831

  url = {http://www.springerlink.com/content/74bxqmgu9uted4fq}

4832

4833

4834

@INPROCEEDINGS{Rokicki1994,

4835

  author = {Tomas Rokicki and Chris J. Myers},

4836

  title = {Automatic Verification of Timed Circuits},

4837

  booktitle = {CAV '94: Proceedings of the 6th International Conference on Computer

4838

	Aided Verification},

4839

  year = {1994},

4840

  pages = {468--480},

4841

  address = {London, UK},

4842

  publisher = {Springer-Verlag},

4843

  isbn = {3-540-58179-0},

4844

  owner = {harald},

4845

  timestamp = {2009.09.18}

4846

4847

4848

@TECHREPORT{Ronkko1997,

4849

  author = {Ronkko, Mauno and Ravn, Anders P.},

4850

  title = {Switches and Jumps in Hybrid Action Systems},

4851

  year = {1997},

4852

  publisher = {Turku Centre for Computer Science},

4853

  source = {http://www.ncstrl.org:8900/ncstrl/servlet/search?formname=detail\&id=oai%3Ancstrlh%3Atucs_fi%3Ancstrl.tucs.fi%2F%2FTUCS-TR-152}

4854

4855

4856

@BOOK{Roscoe1997,

4857

  title = {The Theory and Practice of Concurrency},

4858

  publisher = {Prentice Hall PTR},

4859

  year = {1997},

4860

  author = {Roscoe, A. W. and Hoare, C. A. R. and Bird, Richard},

4861

  address = {Upper Saddle River, NJ, USA},

4862

  isbn = {0136744095}

4863

4864

4865

@BOOK{Rumbaugh2004,

4866

  title = {The Unified Modeling Language Reference Manual},

4867

  publisher = {Addison--Wesley},

4868

  year = {2004},

4869

  author = {James Rumbaugh and Ivar Jacobson and Grady Booch},

4870

  edition = {2nd},

4871

  owner = {harald},

4872

  timestamp = {2009.09.18}

4873

4874

4875

@BOOK{Rumbaugh2004a,

4876

  title = {Unified Modeling Language Reference Manual, The (2nd Edition)},

4877

  publisher = {Pearson Higher Education},

4878

  year = {2004},

4879

  author = {Rumbaugh, James and Jacobson, Ivar and Booch, Grady},

4880

  isbn = {0321245628}

4881

4882

4883

@BOOK{Russell2002,

4884

  title = {Artificial Intelligence: A Modern Approach (2nd Edition)},

4885

  publisher = {{Prentice Hall}},

4886

  year = {2002},

4887

  author = {Russell, Stuart J. and Norvig, Peter },

4888

  howpublished = {Hardcover},

4889

  isbn = {0137903952},

4890

  owner = {harald},

4891

  timestamp = {2009.09.18}

4892

4893

4894

@ARTICLE{Say2003,

4895

  author = {Say, A. C. Cem and Akin, H. Levent},

4896

  title = {Sound and complete qualitative simulation is impossible},

4897

  journal = {Artif. Intell.},

4898

  year = {2003},

4899

  volume = {149},

4900

  pages = {251--266},

4901

  number = {2},

4902

  address = {Essex, UK},

4903

  doi = {http://dx.doi.org/10.1016/S0004-3702(03)00077-8},

4904

  issn = {0004-3702},

4905

  publisher = {Elsevier Science Publishers Ltd.}

4906

4907

4908

@INPROCEEDINGS{Schlatte2008,

4909

  author = {Rudolf Schlatte and Bernhard Aichernig and Frank de Boer and Andreas

4910

	Griesmayer and Einar Broch Johnsen},

4911

  title = {Testing Concurrent Objects with Application-Specific Schedulers},

4912

  year = {2008},

4913

  series = {LNCS},

4914

  publisher = {Springer-Verlag},

4915

  note = {To be published in the proceedings for ICTAC 2008},

4916

  abstract = {In this paper, we propose a novel approach to testing executable models

4917

	of concurrent objects under application-specific scheduling regimes.

4918

	Method activations in concurrent objects are modelled as a composition

4919

	of symbolic automata; this composition expresses all possible interleavings

4920

	of actions. Scheduler specifications, also modelled as automata,

4921

	are used to constrain the system execution. Test purposes are expressed

4922

	as assertions on selected states of the system, and weakest precondition

4923

	calculation is used to derive the test cases from these test purposes.

4924

	Our new testing technique is based on the assumption that we have

4925

	full control over the (application-specific) scheduler, which is

4926

	the case in our executable models under test. Hence, the enforced

4927

	scheduling policy becomes an integral part of a test case. This tackles

4928

	the problem of testing non-deterministic behaviour due to scheduling.},

4929

  owner = {harald},

4930

  timestamp = {2009.09.18}

4931

4932

4933

@TECHREPORT{Sekerinski1996,

4934

  author = {Sekerinski, Emil and Sere, Kaisa},

4935

  title = {A Theory of Prioritizing Composition},

4936

  year = {1996},

4937

  publisher = {Turku Centre for Computer Science},

4938

  source = {http://www.ncstrl.org:8900/ncstrl/servlet/search?formname=detail\&id=oai%3Ancstrlh%3Atucs_fi%3Ancstrl.tucs.fi%2F%2FTUCS-TR-5}

4939

4940

4941

@INPROCEEDINGS{Sen2005a,

4942

  author = {Sen, Koushik and Marinov, Darko and Agha, Gul },

4943

  title = {CUTE: a concolic unit testing engine for C},

4944

  booktitle = {ESEC/FSE-13: Proceedings of the 10th European software engineering

4945

	conference held jointly with 13th ACM SIGSOFT international symposium

4946

	on Foundations of software engineering},

4947

  year = {2005},

4948

  pages = {263--272},

4949

  address = {New York, NY, USA},

4950

  publisher = {ACM},

4951

  abstract = {In unit testing, a program is decomposed into units which are collections

4952

	of functions. A part of unit can be tested by generating inputs for

4953

	a single entry function. The entry function may contain pointer arguments,

4954

	in which case the inputs to the unit are memory graphs. The paper

4955

	addresses the problem of automating unit testing with memory graphs

4956

	as inputs. The approach used builds on previous work combining symbolic

4957

	and concrete execution, and more specifically, using such a combination

4958

	to generate test inputs to explore all feasible execution paths.

4959

	The current work develops a method to represent and track constraints

4960

	that capture the behavior of a symbolic execution of a unit with

4961

	memory graphs as inputs. Moreover, an efficient constraint solver

4962

	is proposed to facilitate incremental generation of such test inputs.

4963

	Finally, CUTE, a tool implementing the method is described together

4964

	with the results of applying CUTE to real-world examples of C code.},

4965

  citeulike-article-id = {2236218},

4966

  doi = {10.1145/1081706.1081750},

4967

  isbn = {1595930140},

4968

  keywords = {c, concolic, testing},

4969

  owner = {harald},

4970

  posted-at = {2008-04-15 08:49:28},

4971

  priority = {2},

4972

  timestamp = {2009.09.18},

4973

  url = {http://portal.acm.org/citation.cfm?id=1081750}

4974

4975

4976

@ARTICLE{Sims2007,

4977

  author = {Sims, S. and DuVarney, D.C.},

4978

  title = {{Experience report: the reactis validation tool}},

4979

  journal = {Proceedings of the 2007 ACM SIGPLAN international conference on Functional

4980

	programming},

4981

  year = {2007},

4982

  pages = {137--140},

4983

  owner = {harald},

4984

  publisher = {ACM Press New York, NY, USA},

4985

  timestamp = {2009.09.18}

4986

4987

4988

@ARTICLE{Slaughter1998,

4989

  author = {Sandra A. Slaughter and Donald E. Harter and Mayuram S. Krishnan},

4990

  title = {Evaluating the cost of software quality},

4991

  journal = {Commun. ACM},

4992

  year = {1998},

4993

  volume = {41},

4994

  pages = {67--73},

4995

  number = {8},

4996

  address = {New York, NY, USA},

4997

  doi = {http://doi.acm.org/10.1145/280324.280335},

4998

  issn = {0001-0782},

4999

  owner = {harald},

5000

  publisher = {ACM},

5001

  timestamp = {2009.09.18}

5002

5003

5004

@BOOK{Stewart1977,

5005

  title = {The Foundations of Mathematics},

5006

  publisher = {Oxford University Press},

5007

  year = {1977},

5008

  author = {Ian Stewart and David Tall},

5009

  owner = {harald},

5010

  timestamp = {2010.11.03}

5011

5012

5013

@ARTICLE{TaiAug1996,

5014

  author = {Tai, Kuo C. },

5015

  title = {Theory of fault-based predicate testing for computer programs},

5016

  journal = {Software Engineering, Transactions on},

5017

  year = {Aug 1996},

5018

  volume = {22},

5019

  pages = {552--562},

5020

  number = {8},

5021

  abstract = {Predicates appear in both the specification and implementation of

5022

	a program. One approach to software testing, referred to as predicate

5023

	testing, is to require certain types of tests for a predicate. In

5024

	this paper, three fault-based testing criteria are defined for compound

5025

	predicates, which are predicates with one or more AND/OR operators.

5026

	BOR (boolean operator) testing requires a set of tests to guarantee

5027

	the detection of (single or multiple) boolean operator faults, including

5028

	incorrect AND/OR operators and missing/extra NOT operators. BRO (boolean

5029

	and relational operator) testing requires a set of tests to guarantee

5030

	the detection of boolean operator faults and relational operator

5031

	faults (i.e., incorrect relational operators). BRE (boolean and relational

5032

	expression) testing requires a set of tests to guarantee the detection

5033

	of boolean operator faults, relational operator faults, and a type

5034

	of fault involving arithmetical expressions. It is shown that for

5035

	a compound predicate with n, n>0, AND/OR operators, at most n+2 constraints

5036

	are needed for BOR testing and at most 2*n+3 constraints for BRO

5037

	or BRE testing, where each constraint specifies a restriction on

5038

	the value of each boolean variable or relational expression in the

5039

	predicate. Algorithms for generating a minimum set of constraints

5040

	for BOR, BRO, and BRE testing of a compound predicate are given,

5041

	and the feasibility problem for the generated constraints is discussed.

5042

	For boolean expressions that contain multiple occurrences of some

5043

	boolean variables, how to combine BOR testing with the meaningful

5044

	impact strategy (Weyuker et al., 1994) is described},

5045

  citeulike-article-id = {2637997},

5046

  doi = {10.1109/32.536956},

5047

  keywords = {arithmetical, bibtex-import, boolean, bor, bre, bro, compound, debugging,

5048

	expression, expressions, fault-based, faults, feasibility, formal,

5049

	functions, impact, implementation, meaningful, not, operator, operators,

5050

	predicate, predicates, problem, program, programming, relational,

5051

	specification, strategy, testing, theoryandor, variable},

5052

  owner = {harald},

5053

  posted-at = {2008-04-07 16:23:42},

5054

  priority = {2},

5055

  timestamp = {2009.09.18},

5056

  url = {http://dx.doi.org/10.1109/32.536956}

5057

5058

5059

@ARTICLE{Tai17-21May1993,

5060

  author = {Tai, K. C. },

5061

  title = {Predicate-based test generation for computer programs},

5062

  journal = {Software Engineering, 1993. Proceedings., 15th International Conference

5063

	on},

5064

  year = {17-21 May 1993},

5065

  pages = {267--276},

5066

  citeulike-article-id = {2637996},

5067

  doi = {10.1109/ICSE.1993.346037},

5068

  keywords = {and, andor, bibtex-import, boolean, compound, correctness, fault-based,

5069

	functions, operator, operators, predicates, program, relational,

5070

	simple, strategies, testing},

5071

  local-url = {file://localhost/Users/michele/mogentes/bibliography/00346037.pdf},

5072

  owner = {harald},

5073

  posted-at = {2008-04-07 16:23:42},

5074

  priority = {2},

5075

  timestamp = {2009.09.18},

5076

  url = {http://dx.doi.org/10.1109/ICSE.1993.346037}

5077

5078

5079

@INPROCEEDINGS{Tan2004,

5080

  author = {Li Tan and Oleg Sokolsky and Insup Lee},

5081

  title = {Specification-based Testing with Linear Temporal Logic},

5082

  booktitle = {Proceedings of IEEE International Conference on Information Reuse

5083

	and Integration (IRI'04)},

5084

  year = {2004},

5085

  pages = {493--498},

5086

  owner = {gordon},

5087

  timestamp = {2006.02.20}

5088

5089

5090

@INPROCEEDINGS{Tiwari2002,

5091

  author = {Tiwari, Ashish and Khanna, Gaurav},

5092

  title = {Series of Abstractions for Hybrid Automata},

5093

  booktitle = {Hybrid Systems: Computation and Control},

5094

  year = {2002},

5095

  editor = {Tomlin, Claire and Greenstreet, Mark},

5096

  volume = {2289},

5097

  series = {Lecture Notes in Computer Science},

5098

  pages = {425-438},

5099

  publisher = {Springer Berlin, Heidelberg},

5100

  affiliation = {SRI International 333 Ravenswood Ave Menlo Park CA USA},

5101

  url = {http://dx.doi.org/10.1007/3-540-45873-5_36}

5102

5103

5104

@ARTICLE{Tomlin1998,

5105

  author = {Tomlin, C. and Pappas, G.J. and Sastry, S.},

5106

  title = {Conflict resolution for air traffic management: a study in multiagent

5107

	hybrid systems},

5108

  journal = {Automatic Control, IEEE Transactions on},

5109

  year = {1998},

5110

  volume = {43},

5111

  pages = {509 -521},

5112

  number = {4},

5113

  month = apr,

5114

  doi = {10.1109/9.664154},

5115

  issn = {0018-9286}

5116

5117

5118

@INPROCEEDINGS{Tretmans2008,

5119

  author = {Jan Tretmans},

5120

  title = {Model Based Testing with Labelled Transition Systems},

5121

  booktitle = {Formal Methods and Testing},

5122

  year = {2008},

5123

  editor = {R.M. Hierons and J.P. Bowen and M. Harman},

5124

  volume = {4949},

5125

  series = {Lecture Notes in Computer Science},

5126

  pages = {1--38},

5127

  publisher = {Springer},

5128

  comment = {p},

5129

  file = {tretmans2008model.pdf:tretmans2008model.pdf:PDF},

5130

  owner = {martin},

5131

  timestamp = {2008.03.13}

5132

5133

5134

@INPROCEEDINGS{Tretmans1996,

5135

  author = {Tretmans, Jan },

5136

  title = {Test Generation with Inputs, Outputs, and Quiescence},

5137

  booktitle = {TACAs '96: Proceedings of the Second International Workshop on Tools

5138

	and Algorithms for Construction and Analysis of Systems},

5139

  year = {1996},

5140

  pages = {127--146},

5141

  address = {London, UK},

5142

  publisher = {Springer-Verlag},

5143

  citeulike-article-id = {1467403},

5144

  isbn = {3540610421},

5145

  keywords = {complete, exhaustive, ioconf, sound},

5146

  owner = {harald},

5147

  posted-at = {2008-04-07 15:37:05},

5148

  priority = {0},

5149

  timestamp = {2009.09.18},

5150

  url = {http://portal.acm.org/citation.cfm?id=693775}

5151

5152

5153

@ARTICLE{Tretmans1996a,

5154

  author = {Jan Tretmans},

5155

  title = {Test Generation with Inputs, Outputs and Repetitive Quiescence.},

5156

  journal = {Software - Concepts and Tools},

5157

  year = {1996},

5158

  volume = {17},

5159

  pages = {103--120},

5160

  number = {3},

5161

  comment = {p,r},

5162

  file = {tretmans1996testgeneration.pdf:tretmans1996testgeneration.pdf:PDF},

5163

  keywords = {ioco},

5164

  owner = {martin},

5165

  timestamp = {2007.07.31}

5166

5167

5168

@INPROCEEDINGS{Tretmans2003,

5169

  author = {Jan Tretmans and Ed Brinksma},

5170

  title = {{TorX}: Automated Model Based Testing},

5171

  booktitle = {Proceedings of the 1st European Conference on Model-Driven Software

5172

	Engineering},

5173

  year = {2003},

5174

  editor = {A. Hartman and K. Dussa-Zieger},

5175

  pages = {13--25},

5176

  address = {Nurnburg, Germany},

5177

  abstract = {Similar to the TGV-Tool, this tool relaies on the IOCO-Relation for

5178

	test generation. There are two main differences. The first one is

5179

	, that TorX does not produce a test case but sends Input-Sequences

5180

	directly to the IUT while construction the LTS. The second one is

5181

	that TorX does not use a test purpose but generates the test sequence

5182

	randomly.},

5183

  comment = {p,r},

5184

  file = {tretmans2003torx.pdf:tretmans2003torx.pdf:PDF},

5185

  filename = {./test\_generation/trej2003-torx.pdf},

5186

  keywords = {Testing, Conformance Test, Test generation, I/O LTS},

5187

  owner = {harald},

5188

  timestamp = {2009.09.18}

5189

5190

5191

@BOOK{Utting2006,

5192

  title = {Practical Model-Based Testing: A Tools Approach},

5193

  publisher = {Morgan Kaufmann Publishers Inc.},

5194

  year = {2006},

5195

  author = {Utting, Mark and Legeard, Bruno },

5196

  address = {San Francisco, CA, USA},

5197

  citeulike-article-id = {2637985},

5198

  keywords = {bibtex-import, tug},

5199

  owner = {harald},

5200

  posted-at = {2008-04-07 16:23:40},

5201

  priority = {2},

5202

  timestamp = {2009.09.18}

5203

5204

5205

@INPROCEEDINGS{Vanzin2006,

5206

  author = {Daniel D. Vanzin and Ivan L. Martins and Joao Bosco A. Pereira Filho},

5207

  title = {TDE UML Editor - A Success Development Case of a Software Extension},

5208

  booktitle = {ICGSE '06: Proceedings of the IEEE international conference on Global

5209

	Software Engineering},

5210

  year = {2006},

5211

  pages = {257--258},

5212

  address = {Washington, DC, USA},

5213

  publisher = {IEEE Computer Society},

5214

  isbn = {0-7695-2663-2},

5215

  owner = {harald},

5216

  timestamp = {2009.09.18}

5217

5218

5219

@BOOK{Warmer1998,

5220

  title = {The {Object Constraint Language}: Precise Modeling with {UML}},

5221

  publisher = {Addison-Wesley},

5222

  year = {1998},

5223

  author = {Jos Warmer and Anneke Kleppe},

5224

  isbn = {0-201-37940-6},

5225

  owner = {harald},

5226

  timestamp = {2009.09.18}

5227

5228

5229

@INPROCEEDINGS{Weiglhofer2008,

5230

  author = {Martin Weiglhofer and Franz Wotawa},

5231

  title = {Random vs. Scenario-Based vs. Fault-Based Testing -- An Industrial

5232

	Evaluation of Formal Black-Box Testing Methods},

5233

  booktitle = {Proceedings of the 3rd International Conference on Evaluation of

5234

	Novel Approaches to Software Engineering},

5235

  year = {2008},

5236

  owner = {harald},

5237

  timestamp = {2009.09.18}

5238

5239

5240

@INPROCEEDINGS{Weiglhofer2008a,

5241

  author = {Martin Weiglhofer and Franz Wotawa},

5242

  title = {"{O}n the fly" input output conformance verification},

5243

  booktitle = {Proceedings of the IASTED International Conference on Software Engineering},

5244

  year = {2008},

5245

  address = {Innsbruck, Austria},

5246

  month = {February},

5247

  note = {To appear.},

5248

  comment = {a},

5249

  file = {weiglhofer2008onthefly.pdf:weiglhofer2008onthefly.pdf:PDF},

5250

  owner = {martin},

5251

  timestamp = {2007.10.09}

5252

5253

5254

@INPROCEEDINGS{Wong2010,

5255

  author = {Wong, W.E. and Debroy, V. and Surampudi, A. and HyeonJeong Kim and

5256

	Siok, M.F.},

5257

  title = {Recent Catastrophic Accidents: Investigating How Software was Responsible},

5258

  booktitle = {Secure Software Integration and Reliability Improvement (SSIRI),

5259

	2010 Fourth International Conference on},

5260

  year = {2010},

5261

  pages = {14 -22},

5262

  month = june,

5263

  doi = {10.1109/SSIRI.2010.38},

5264

  keywords = {accident avoidance;causative factor;recent catastrophic accidents;safety-critical

5265

	software;safety-critical software;}

5266

5267

5268

@INPROCEEDINGS{Wotawa2007,

5269

  author = {Franz Wotawa},

5270

  title = {Generating test-cases from qualitative knowledge -- Preliminary report},

5271

  booktitle = {Proceedings of the 21st Annual Workshop on Qualitative Reasoning},

5272

  year = {2007},

5273

  address = {Aberystwyth, U.K.},

5274

  month = {June},

5275

  owner = {harald},

5276

  timestamp = {2009.09.18}

5277

5278

5279

@ARTICLE{Xie2007,

5280

  author = {Qing Xie and Atif M. Memon},

5281

  title = {Designing and comparing automated test oracles for GUI-based software

5282

	applications},

5283

  journal = {ACM Trans. Softw. Eng. Methodol.},

5284

  year = {2007},

5285

  volume = {16},

5286

  number = {1},

5287

  bibsource = {DBLP, http://dblp.uni-trier.de},

5288

  ee = {http://doi.acm.org/10.1145/1189748.1189752},

5289

  owner = {harald},

5290

  timestamp = {2009.09.18}

5291

5292

5293

@ARTICLE{Yates1989,

5294

  author = {Yates, D. and Malevris, N. },

5295

  title = {Reducing the effects of infeasible paths in branch testing},

5296

  journal = {SIGSOFT Softw. Eng. Notes},

5297

  year = {1989},

5298

  volume = {14},

5299

  pages = {48--54},

5300

  number = {8},

5301

  address = {New York, NY, USA},

5302

  citeulike-article-id = {2637995},

5303

  doi = {http://doi.acm.org/10.1145/75309.75315},

5304

  keywords = {bibtex-import},

5305

  local-url = {file://localhost/Users/michele/mogentes/bibliography/p48-yates.pdf},

5306

  owner = {harald},

5307

  posted-at = {2008-04-07 16:23:42},

5308

  priority = {2},

5309

  publisher = {ACM},

5310

  timestamp = {2009.09.18},

5311

  url = {http://dx.doi.org/10.1145/75309.75315}

5312

5313

5314

@BOOK{Young2005,

5315

  title = {Software Testing and Analysis: Process, Principles and Techniques},

5316

  publisher = {John Wiley \& Sons},

5317

  year = {2005},

5318

  author = {Young, Michal and Pezze, Mauro },

5319

  citeulike-article-id = {2638003},

5320

  keywords = {bibtex-import, coverage, criteriainfeasibility, problem},

5321

  owner = {harald},

5322

  posted-at = {2008-04-07 16:23:44},

5323

  priority = {2},

5324

  timestamp = {2009.09.18}

5325

5326

5327

@PROCEEDINGS{Alur2003,

5328

  title = {Embedded Software, Third International Conference, EMSOFT 2003, Philadelphia,

5329

	PA, USA, October 13-15, 2003, Proceedings},

5330

  year = {2003},

5331

  editor = {Rajeev Alur and Insup Lee},

5332

  volume = {2855},

5333

  series = {Lecture Notes in Computer Science},

5334

  publisher = {Springer},

5335

  bibsource = {DBLP, http://dblp.uni-trier.de},

5336

  booktitle = {EMSOFT},

5337

  isbn = {3-540-20223-4},

5338

  owner = {harald},

5339

  timestamp = {2009.09.18}

5340

5341

5342

@PROCEEDINGS{Arabnia2007,

5343

  title = {Proceedings of the 2007 International Conference on Software Engineering

5344

	Research {\&} Practice, SERP 2007, Volume II, June 25-28, 2007, Las

5345

	Vegas Nevada, USA},

5346

  year = {2007},

5347

  editor = {Hamid R. Arabnia and Hassan Reza},

5348

  publisher = {CSREA Press},

5349

  bibsource = {DBLP, http://dblp.uni-trier.de},

5350

  booktitle = {Software Engineering Research and Practice},

5351

  isbn = {1-60132-034-5},

5352

  owner = {harald},

5353

  timestamp = {2009.09.18}

5354

5355

5356

@PROCEEDINGS{Avrunin2004,

5357

  title = {Proceedings of the ACM/SIGSOFT International Symposium on Software

5358

	Testing and Analysis, ISSTA 2004, Boston, Massachusetts, USA, July

5359

	11-14, 2004},

5360

  year = {2004},

5361

  editor = {George S. Avrunin and Gregg Rothermel},

5362

  publisher = {ACM},

5363

  bibsource = {DBLP, http://dblp.uni-trier.de},

5364

  booktitle = {ISSTA},

5365

  isbn = {1-58113-820-2},

5366

  owner = {harald},

5367

  timestamp = {2009.09.18}

5368

5369

5370

@PROCEEDINGS{Ball2006a,

5371

  title = {Computer Aided Verification, 18th International Conference, CAV 2006,

5372

	Seattle, WA, USA, August 17-20, 2006, Proceedings},

5373

  year = {2006},

5374

  editor = {Thomas Ball and Robert B. Jones},

5375

  volume = {4144},

5376

  series = {Lecture Notes in Computer Science},

5377

  publisher = {Springer},

5378

  bibsource = {DBLP, http://dblp.uni-trier.de},

5379

  booktitle = {CAV},

5380

  isbn = {3-540-37406-X},

5381

  owner = {harald},

5382

  timestamp = {2009.09.18}

5383

5384

5385

@PROCEEDINGS{Beckert2008,

5386

  title = {Tests and Proofs, Second International Conference, TAP 2008, Prato,

5387

	Italy, April 9-11, 2008. Proceedings},

5388

  year = {2008},

5389

  editor = {Bernhard Beckert and Reiner H{\"a}hnle},

5390

  volume = {4966},

5391

  series = {Lecture Notes in Computer Science},

5392

  publisher = {Springer},

5393

  bibsource = {DBLP, http://dblp.uni-trier.de},

5394

  booktitle = {TAP},

5395

  isbn = {978-3-540-79123-2},

5396

  owner = {harald},

5397

  timestamp = {2009.09.18}

5398

5399

5400

@PROCEEDINGS{Bemporad2007,

5401

  title = {Hybrid Systems: Computation and Control, 10th International Workshop,

5402

	HSCC 2007, Pisa, Italy, April 3-5, 2007, Proceedings},

5403

  year = {2007},

5404

  editor = {Alberto Bemporad and Antonio Bicchi and Giorgio C. Buttazzo},

5405

  volume = {4416},

5406

  series = {Lecture Notes in Computer Science},

5407

  publisher = {Springer},

5408

  bibsource = {DBLP, http://dblp.uni-trier.de},

5409

  booktitle = {HSCC},

5410

  isbn = {978-3-540-71492-7},

5411

  owner = {harald},

5412

  timestamp = {2009.09.18}

5413

5414

5415

@PROCEEDINGS{Berbers2006,

5416

  title = {Proceedings of the 2006 EuroSys Conference, Leuven, Belgium, April

5417

	18-21, 2006},

5418

  year = {2006},

5419

  editor = {Yolande Berbers and Willy Zwaenepoel},

5420

  publisher = {ACM},

5421

  bibsource = {DBLP, http://dblp.uni-trier.de},

5422

  booktitle = {EuroSys},

5423

  isbn = {1-59593-322-0},

5424

  owner = {harald},

5425

  timestamp = {2009.09.18}

5426

5427

5428

@PROCEEDINGS{Bernardo2004,

5429

  title = {Formal Methods for the Design of Real-Time Systems, International

5430

	School on Formal Methods for the Design of Computer, Communication

5431

	and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13-18,

5432

	2004, Revised Lectures},

5433

  year = {2004},

5434

  editor = {Marco Bernardo and Flavio Corradini},

5435

  volume = {3185},

5436

  series = {Lecture Notes in Computer Science},

5437

  publisher = {Springer},

5438

  bibsource = {DBLP, http://dblp.uni-trier.de},

5439

  booktitle = {SFM},

5440

  isbn = {3-540-23068-8},

5441

  owner = {harald},

5442

  timestamp = {2009.09.18}

5443

5444

5445

@PROCEEDINGS{Brim2007,

5446

  title = {Formal Methods: Applications and Technology, 11th International Workshop,

5447

	FMICS 2006 and 5th International Workshop PDMC 2006, Bonn, Germany,

5448

	August 26-27, and August 31, 2006, Revised Selected Papers},

5449

  year = {2007},

5450

  editor = {Lubos Brim and Boudewijn R. Haverkort and Martin Leucker and Jaco

5451

	van de Pol},

5452

  volume = {4346},

5453

  series = {Lecture Notes in Computer Science},

5454

  publisher = {Springer},

5455

  bibsource = {DBLP, http://dblp.uni-trier.de},

5456

  booktitle = {FMICS/PDMC},

5457

  isbn = {978-3-540-70951-0},

5458

  owner = {harald},

5459

  timestamp = {2009.09.18}

5460

5461

5462

@PROCEEDINGS{Broy2005,

5463

  title = {Model-Based Testing of Reactive Systems},

5464

  year = {2005},

5465

  editor = {Manfred Broy and Bengt Jonsson and Joost-Pieter Katoen and Martin

5466

	Leucker and Alexander Pretschner},

5467

  volume = {3472},

5468

  series = {Lecture Notes in Computer Science},

5469

  publisher = {Springer},

5470

  bibsource = {DBLP, http://dblp.uni-trier.de},

5471

  booktitle = {Model-Based Testing of Reactive Systems},

5472

  isbn = {3-540-26278-4},

5473

  owner = {harald},

5474

  timestamp = {2009.09.18}

5475

5476

5477

@BOOK{Buxton1970,

5478

  title = {Software Engineering Techniques: Report of a conference sponsored

5479

	by the NATO Science Committee, Rome, Italy, 27-31 Oct. 1969, Brussels,

5480

	Scientific Affairs Division, NATO},

5481

  year = {1970},

5482

  editor = {Buxton, J. N. and Randell, B.}

5483

5484

5485

@PROCEEDINGS{Cassez2001,

5486

  title = {Modeling and Verification of Parallel Processes, 4th Summer School,

5487

	MOVEP 2000, Nantes, France, June 19-23, 2000},

5488

  year = {2001},

5489

  editor = {Franck Cassez and Claude Jard and Brigitte Rozoy and Mark Dermot

5490

	Ryan},

5491

  volume = {2067},

5492

  series = {Lecture Notes in Computer Science},

5493

  publisher = {Springer},

5494

  bibsource = {DBLP, http://dblp.uni-trier.de},

5495

  booktitle = {MOVEP},

5496

  isbn = {3-540-42787-2},

5497

  owner = {harald},

5498

  timestamp = {2009.09.18}

5499

5500

5501

@PROCEEDINGS{Chechik2009,

5502

  title = {Fundamental Approaches to Software Engineering, 12th International

5503

	Conference, FASE 2009, Held as Part of the Joint European Conferences

5504

	on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29,

5505

	2009. Proceedings},

5506

  year = {2009},

5507

  editor = {Marsha Chechik and Martin Wirsing},

5508

  volume = {5503},

5509

  series = {Lecture Notes in Computer Science},

5510

  publisher = {Springer},

5511

  bibsource = {DBLP, http://dblp.uni-trier.de},

5512

  booktitle = {FASE},

5513

  ee = {http://dx.doi.org/10.1007/978-3-642-00593-0},

5514

  isbn = {978-3-642-00592-3},

5515

  owner = {harald},

5516

  timestamp = {2009.09.18}

5517

5518

5519

@PROCEEDINGS{Cin2005,

5520

  title = {Dependable Computing - EDCC-5, 5th European Dependable Computing

5521

	Conference, Budapest, Hungary, April 20-22, 2005, Proceedings},

5522

  year = {2005},

5523

  editor = {Mario Dal Cin and Mohamed Ka{\^a}niche and Andr{\'a}s Pataricza},

5524

  volume = {3463},

5525

  series = {Lecture Notes in Computer Science},

5526

  publisher = {Springer},

5527

  bibsource = {DBLP, http://dblp.uni-trier.de},

5528

  booktitle = {EDCC},

5529

  isbn = {3-540-25723-3},

5530

  owner = {harald},

5531

  timestamp = {2009.09.18}

5532

5533

5534

@PROCEEDINGS{Damm2007,

5535

  title = {Computer Aided Verification, 19th International Conference, CAV 2007,

5536

	Berlin, Germany, July 3-7, 2007, Proceedings},

5537

  year = {2007},

5538

  editor = {Werner Damm and Holger Hermanns},

5539

  volume = {4590},

5540

  series = {Lecture Notes in Computer Science},

5541

  publisher = {Springer},

5542

  bibsource = {DBLP, http://dblp.uni-trier.de},

5543

  booktitle = {CAV},

5544

  isbn = {978-3-540-73367-6},

5545

  owner = {harald},

5546

  timestamp = {2009.09.18}

5547

5548

5549

@BOOK{DangVan2002,

5550

  title = {Specification case studies in RAISE},

5551

  publisher = {Springer-Verlag},

5552

  year = {2002},

5553

  editor = {Dang Van, H. and George, C. and Janowski, T. and Moore, R. },

5554

  address = {London, UK},

5555

  isbn = {1-85233-359-6},

5556

  owner = {harald},

5557

  timestamp = {2009.09.18}

5558

5559

5560

@PROCEEDINGS{Dershowitz2003,

5561

  title = {Verification: Theory and Practice, Essays Dedicated to Zohar Manna

5562

	on the Occasion of His 64th Birthday},

5563

  year = {2003},

5564

  editor = {Nachum Dershowitz},

5565

  volume = {2772},

5566

  series = {Lecture Notes in Computer Science},

5567

  publisher = {Springer},

5568

  bibsource = {DBLP, http://dblp.uni-trier.de},

5569

  booktitle = {Verification: Theory and Practice},

5570

  isbn = {3-540-21002-4},

5571

  owner = {harald},

5572

  timestamp = {2009.09.18}

5573

5574

5575

@PROCEEDINGS{Dacker2003,

5576

  title = {Proceedings of the 2003 ACM SIGPLAN Workshop on Erlang, Uppsala,

5577

	Sweden, August 29, 2003},

5578

  year = {2003},

5579

  editor = {Bjarne D{\"a}cker and Thomas Arts},

5580

  publisher = {ACM},

5581

  bibsource = {DBLP, http://dblp.uni-trier.de},

5582

  booktitle = {Erlang Workshop},

5583

  isbn = {1-58113-772-9},

5584

  owner = {harald},

5585

  timestamp = {2009.09.18}

5586

5587

5588

@PROCEEDINGS{Fitzgerald2005,

5589

  title = {FM 2005: Formal Methods, International Symposium of Formal Methods

5590

	Europe, Newcastle, UK, July 18-22, 2005, Proceedings},

5591

  year = {2005},

5592

  editor = {John Fitzgerald and Ian J. Hayes and Andrzej Tarlecki},

5593

  volume = {3582},

5594

  series = {Lecture Notes in Computer Science},

5595

  publisher = {Springer},

5596

  bibsource = {DBLP, http://dblp.uni-trier.de},

5597

  booktitle = {FM},

5598

  isbn = {3-540-27882-6},

5599

  owner = {harald},

5600

  timestamp = {2009.09.18}

5601

5602

5603

@PROCEEDINGS{Garavel2003,

5604

  title = {Tools and Algorithms for the Construction and Analysis of Systems,

5605

	9th International Conference, TACAS 2003, Held as Part of the Joint

5606

	European Conferences on Theory and Practice of Software, ETAPS 2003,

5607

	Warsaw, Poland, April 7-11, 2003, Proceedings},

5608

  year = {2003},

5609

  editor = {Hubert Garavel and John Hatcliff},

5610

  volume = {2619},

5611

  series = {Lecture Notes in Computer Science},

5612

  publisher = {Springer},

5613

  bibsource = {DBLP, http://dblp.uni-trier.de},

5614

  booktitle = {TACAS},

5615

  isbn = {3-540-00898-5},

5616

  owner = {harald},

5617

  timestamp = {2009.09.18}

5618

5619

5620

@PROCEEDINGS{Grabowski2005,

5621

  title = {Formal Approaches to Software Testing, 4th International Workshop,

5622

	FATES 2004, Linz, Austria, September 21, 2004, Revised Selected Papers},

5623

  year = {2005},

5624

  editor = {Jens Grabowski and Brian Nielsen},

5625

  volume = {3395},

5626

  series = {Lecture Notes in Computer Science},

5627

  publisher = {Springer},

5628

  bibsource = {DBLP, http://dblp.uni-trier.de},

5629

  booktitle = {FATES},

5630

  isbn = {3-540-25109-X},

5631

  owner = {harald},

5632

  timestamp = {2009.09.18}

5633

5634

5635

@PROCEEDINGS{Grieskamp2000,

5636

  title = {Integrated Formal Methods, Second International Conference, IFM 2000,

5637

	Dagstuhl Castle, Germany, November 1-3, 2000, Proceedings},

5638

  year = {2000},

5639

  editor = {Wolfgang Grieskamp and Thomas Santen and Bill Stoddart},

5640

  volume = {1945},

5641

  series = {Lecture Notes in Computer Science},

5642

  publisher = {Springer},

5643

  bibsource = {DBLP, http://dblp.uni-trier.de},

5644

  booktitle = {IFM},

5645

  isbn = {3-540-41196-8},

5646

  owner = {harald},

5647

  timestamp = {2009.09.18}

5648

5649

5650

@PROCEEDINGS{Grieskamp2006a,

5651

  title = {Formal Approaches to Software Testing, 5th International Workshop,

5652

	FATES 2005, Edinburgh, UK, July 11, 2005, Revised Selected Papers},

5653

  year = {2006},

5654

  editor = {Wolfgang Grieskamp and Carsten Weise},

5655

  volume = {3997},

5656

  series = {Lecture Notes in Computer Science},

5657

  publisher = {Springer},

5658

  bibsource = {DBLP, http://dblp.uni-trier.de},

5659

  booktitle = {FATES},

5660

  isbn = {3-540-34454-3},

5661

  owner = {harald},

5662

  timestamp = {2009.09.18}

5663

5664

5665

@PROCEEDINGS{Halbwachs2005,

5666

  title = {Tools and Algorithms for the Construction and Analysis of Systems,

5667

	11th International Conference, TACAS 2005, Held as Part of the Joint

5668

	European Conferences on Theory and Practice of Software, ETAPS 2005,

5669

	Edinburgh, UK, April 4-8, 2005, Proceedings},

5670

  year = {2005},

5671

  editor = {Nicolas Halbwachs and Lenore D. Zuck},

5672

  volume = {3440},

5673

  series = {Lecture Notes in Computer Science},

5674

  publisher = {Springer},

5675

  bibsource = {DBLP, http://dblp.uni-trier.de},

5676

  booktitle = {TACAS},

5677

  isbn = {3-540-25333-5},

5678

  owner = {harald},

5679

  timestamp = {2009.09.18}

5680

5681

5682

@PROCEEDINGS{Havelund2006,

5683

  title = {Formal Approaches to Software Testing and Runtime Verification, First

5684

	Combined International Workshops, FATES 2006 and RV 2006, Seattle,

5685

	WA, USA, August 15-16, 2006, Revised Selected Papers},

5686

  year = {2006},

5687

  editor = {Klaus Havelund and Manuel N{\'u}{\~n}ez and Grigore Rosu and Burkhart

5688

	Wolff},

5689

  volume = {4262},

5690

  series = {Lecture Notes in Computer Science},

5691

  publisher = {Springer},

5692

  bibsource = {DBLP, http://dblp.uni-trier.de},

5693

  booktitle = {FATES/RV},

5694

  isbn = {3-540-49699-8},

5695

  owner = {harald},

5696

  timestamp = {2009.09.18}

5697

5698

5699

@PROCEEDINGS{Hierons2008,

5700

  title = {Formal Methods and Testing, An Outcome of the FORTEST Network, Revised

5701

	Selected Papers},

5702

  year = {2008},

5703

  editor = {Robert M. Hierons and Jonathan P. Bowen and Mark Harman},

5704

  volume = {4949},

5705

  series = {Lecture Notes in Computer Science},

5706

  publisher = {Springer},

5707

  bibsource = {DBLP, http://dblp.uni-trier.de},

5708

  booktitle = {Formal Methods and Testing},

5709

  isbn = {978-3-540-78916-1},

5710

  owner = {harald},

5711

  timestamp = {2009.09.18}

5712

5713

5714

@PROCEEDINGS{Juels2006,

5715

  title = {Proceedings of the 13th ACM Conference on Computer and Communications

5716

	Security, CCS 2006, Alexandria, VA, USA, Ioctober 30 - November 3,

5717

	2006},

5718

  year = {2006},

5719

  editor = {Ari Juels and Rebecca N. Wright and Sabrina De Capitani di Vimercati},

5720

  publisher = {ACM},

5721

  bibsource = {DBLP, http://dblp.uni-trier.de},

5722

  booktitle = {ACM Conference on Computer and Communications Security},

5723

  owner = {harald},

5724

  timestamp = {2009.09.18}

5725

5726

5727

@PROCEEDINGS{Karras2007,

5728

  title = {International Conference on Software Engineering Theory and Practice,

5729

	SETP-07, Orlando, Florida, USA, July 9-12 2007},

5730

  year = {2007},

5731

  editor = {Dimitris A. Karras and Daming Wei and Jaroslav Zendulka},

5732

  publisher = {ISRST},

5733

  bibsource = {DBLP, http://dblp.uni-trier.de},

5734

  booktitle = {SETP},

5735

  isbn = {978-0-9727412-6-2},

5736

  owner = {harald},

5737

  timestamp = {2009.09.18}

5738

5739

5740

@PROCEEDINGS{Katoen2002,

5741

  title = {Tools and Algorithms for the Construction and Analysis of Systems,

5742

	8th International Conference, TACAS 2002, Held as Part of the Joint

5743

	European Conference on Theory and Practice of Software, ETAPS 2002,

5744

	Grenoble, France, April 8-12, 2002, Proceedings},

5745

  year = {2002},

5746

  editor = {Joost-Pieter Katoen and Perdita Stevens},

5747

  volume = {2280},

5748

  series = {Lecture Notes in Computer Science},

5749

  publisher = {Springer},

5750

  bibsource = {DBLP, http://dblp.uni-trier.de},

5751

  booktitle = {TACAS},

5752

  isbn = {3-540-43419-4},

5753

  owner = {harald},

5754

  timestamp = {2009.09.18}

5755

5756

5757

@PROCEEDINGS{Kaagstrom1998,

5758

  title = {Applied Parallel Computing, Large Scale Scientific and Industrial

5759

	Problems, 4th International Workshop, PARA '98, Ume{\aa}, Sweden,

5760

	June 14-17, 1998, Proceedings},

5761

  year = {1998},

5762

  editor = {Bo K{\aa}gstr{\"o}m and Jack Dongarra and Erik Elmroth and Jerzy

5763

	Wasniewski},

5764

  volume = {1541},

5765

  series = {Lecture Notes in Computer Science},

5766

  publisher = {Springer},

5767

  bibsource = {DBLP, http://dblp.uni-trier.de},

5768

  booktitle = {PARA},

5769

  isbn = {3-540-65414-3},

5770

  owner = {harald},

5771

  timestamp = {2009.09.18}

5772

5773

5774

@PROCEEDINGS{Lamsweerde1991,

5775

  title = {ESEC '91, 3rd European Software Engineering Conference, Milan, Italy,

5776

	October 21-24, 1991, Proceedings},

5777

  year = {1991},

5778

  editor = {Axel van Lamsweerde and Alfonso Fugetta},

5779

  volume = {550},

5780

  series = {Lecture Notes in Computer Science},

5781

  publisher = {Springer},

5782

  bibsource = {DBLP, http://dblp.uni-trier.de},

5783

  booktitle = {ESEC},

5784

  isbn = {3-540-54742-8},

5785

  owner = {harald},

5786

  timestamp = {2009.09.18}

5787

5788

5789

@PROCEEDINGS{Leucker2009,

5790

  title = {Theoretical Aspects of Computing - ICTAC 2009, 6th International

5791

	Colloquium, Kuala Lumpur, Malaysia, August 16-20, 2009. Proceedings},

5792

  year = {2009},

5793

  editor = {Martin Leucker and Carroll Morgan},

5794

  volume = {5684},

5795

  series = {Lecture Notes in Computer Science},

5796

  publisher = {Springer},

5797

  bibsource = {DBLP, http://dblp.uni-trier.de},

5798

  booktitle = {ICTAC},

5799

  ee = {http://dx.doi.org/10.1007/978-3-642-03466-4},

5800

  isbn = {978-3-642-03465-7},

5801

  owner = {harald},

5802

  timestamp = {2009.09.18}

5803

5804

5805

@PROCEEDINGS{Misra2006,

5806

  title = {FM 2006: Formal Methods, 14th International Symposium on Formal Methods,

5807

	Hamilton, Canada, August 21-27, 2006, Proceedings},

5808

  year = {2006},

5809

  editor = {Jayadev Misra and Tobias Nipkow and Emil Sekerinski},

5810

  volume = {4085},

5811

  series = {Lecture Notes in Computer Science},

5812

  publisher = {Springer},

5813

  bibsource = {DBLP, http://dblp.uni-trier.de},

5814

  booktitle = {FM},

5815

  isbn = {3-540-37215-6},

5816

  owner = {harald},

5817

  timestamp = {2009.09.18}

5818

5819

5820

@PROCEEDINGS{Mosses1995,

5821

  title = {TAPSOFT'95: Theory and Practice of Software Development, 6th International

5822

	Joint Conference CAAP/FASE, Aarhus, Denmark, May 22-26, 1995, Proceedings},

5823

  year = {1995},

5824

  editor = {Peter D. Mosses and Mogens Nielsen and Michael I. Schwartzbach},

5825

  volume = {915},

5826

  series = {Lecture Notes in Computer Science},

5827

  publisher = {Springer},

5828

  bibsource = {DBLP, http://dblp.uni-trier.de},

5829

  booktitle = {TAPSOFT},

5830

  isbn = {3-540-59293-8},

5831

  owner = {harald},

5832

  timestamp = {2009.09.18}

5833

5834

5835

@PROCEEDINGS{Petrenko2007,

5836

  title = {Testing of Software and Communicating Systems, 19th IFIP TC6/WG6.1

5837

	International Conference, TestCom 2007, 7th International Workshop,

5838

	FATES 2007, Tallinn, Estonia, June 26-29, 2007, Proceedings},

5839

  year = {2007},

5840

  editor = {Alexandre Petrenko and Margus Veanes and Jan Tretmans and Wolfgang

5841

	Grieskamp},

5842

  volume = {4581},

5843

  series = {Lecture Notes in Computer Science},

5844

  publisher = {Springer},

5845

  bibsource = {DBLP, http://dblp.uni-trier.de},

5846

  booktitle = {TestCom/FATES},

5847

  isbn = {978-3-540-73065-1},

5848

  owner = {harald},

5849

  timestamp = {2009.09.18}

5850

5851

5852

@PROCEEDINGS{Rafiq1994,

5853

  title = {Protocol Test Systems, VI, Proceedings of the IFIP TC6/WG6.1 Sixth

5854

	International Workshop on Protocol Test systems, Pau, France, 28-30

5855

	September, 1993},

5856

  year = {1994},

5857

  editor = {Omar Rafiq},

5858

  volume = {C-19},

5859

  series = {IFIP Transactions},

5860

  publisher = {North-Holland},

5861

  bibsource = {DBLP, http://dblp.uni-trier.de},

5862

  booktitle = {Protocol Test Systems},

5863

  isbn = {0-444-81697-6},

5864

  owner = {harald},

5865

  timestamp = {2009.09.18}

5866

5867

5868

@PROCEEDINGS{Ramakrishnan2008,

5869

  title = {Tools and Algorithms for the Construction and Analysis of Systems,

5870

	14th International Conference, TACAS 2008, Held as Part of the Joint

5871

	European Conferences on Theory and Practice of Software, ETAPS 2008,

5872

	Budapest, Hungary, March 29-April 6, 2008. Proceedings},

5873

  year = {2008},

5874

  editor = {C. R. Ramakrishnan and Jakob Rehof},

5875

  volume = {4963},

5876

  series = {Lecture Notes in Computer Science},

5877

  publisher = {Springer},

5878

  bibsource = {DBLP, http://dblp.uni-trier.de},

5879

  booktitle = {TACAS},

5880

  isbn = {978-3-540-78799-0},

5881

  owner = {harald},

5882

  timestamp = {2009.09.18}

5883

5884

5885

@PROCEEDINGS{Reed2001,

5886

  title = {SDL 2001: Meeting UML, 10th International SDL Forum Copenhagen, Denmark,

5887

	June 27-29, 2001, Proceedings},

5888

  year = {2001},

5889

  editor = {Rick Reed and Jeanne Reed},

5890

  volume = {2078},

5891

  series = {Lecture Notes in Computer Science},

5892

  publisher = {Springer},

5893

  bibsource = {DBLP, http://dblp.uni-trier.de},

5894

  booktitle = {SDL Forum},

5895

  isbn = {3-540-42281-1},

5896

  owner = {harald},

5897

  timestamp = {2009.09.18}

5898

5899

5900

@PROCEEDINGS{Robby2008,

5901

  title = {30th International Conference on Software Engineering (ICSE 2008),

5902

	Leipzig, Germany, May 10-18, 2008, Companion Volume},

5903

  year = {2008},

5904

  editor = {Robby},

5905

  publisher = {ACM},

5906

  bibsource = {DBLP, http://dblp.uni-trier.de},

5907

  booktitle = {ICSE Companion},

5908

  isbn = {978-1-60558-079-1},

5909

  owner = {harald},

5910

  timestamp = {2009.09.18}

5911

5912

5913

@PROCEEDINGS{Robby2008a,

5914

  title = {30th International Conference on Software Engineering (ICSE 2008),

5915

	Leipzig, Germany, May 10-18, 2008},

5916

  year = {2008},

5917

  editor = {Robby},

5918

  publisher = {ACM},

5919

  bibsource = {DBLP, http://dblp.uni-trier.de},

5920

  booktitle = {ICSE},

5921

  isbn = {978-1-60558-079-1},

5922

  owner = {harald},

5923

  timestamp = {2009.09.18}

5924

5925

5926

@PROCEEDINGS{Sangiorgi1998,

5927

  title = {CONCUR '98: Concurrency Theory, 9th International Conference, Nice,

5928

	France, September 8-11, 1998, Proceedings},

5929

  year = {1998},

5930

  editor = {Davide Sangiorgi and Robert de Simone},

5931

  volume = {1466},

5932

  series = {Lecture Notes in Computer Science},

5933

  publisher = {Springer},

5934

  bibsource = {DBLP, http://dblp.uni-trier.de},

5935

  booktitle = {CONCUR},

5936

  isbn = {3-540-64896-8},

5937

  owner = {harald},

5938

  timestamp = {2009.09.18}

5939

5940

5941

@PROCEEDINGS{Sarkar2005,

5942

  title = {Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language

5943

	Design and Implementation, Chicago, IL, USA, June 12-15, 2005},

5944

  year = {2005},

5945

  editor = {Vivek Sarkar and Mary W. Hall},

5946

  publisher = {ACM},

5947

  bibsource = {DBLP, http://dblp.uni-trier.de},

5948

  booktitle = {PLDI},

5949

  isbn = {1-59593-056-6},

5950

  owner = {harald},

5951

  timestamp = {2009.09.18}

5952

5953

5954

@PROCEEDINGS{Sherratt2003,

5955

  title = {Telecommunications and beyond: The Broader Applicability of SDL and

5956

	MSC, Third International Workshop, SAM 2002, Aberystwyth, UK, June

5957

	24-26, 2002. Revised Papers},

5958

  year = {2003},

5959

  editor = {Edel Sherratt},

5960

  volume = {2599},

5961

  series = {Lecture Notes in Computer Science},

5962

  publisher = {Springer},

5963

  bibsource = {DBLP, http://dblp.uni-trier.de},

5964

  booktitle = {SAM},

5965

  isbn = {3-540-00877-2},

5966

  owner = {harald},

5967

  timestamp = {2009.09.18}

5968

5969

5970

@BOOK{Tretmans2007,

5971

  title = {Tangram: Model-based integration and testing of complex high-tech

5972

	systems},

5973

  publisher = {Embedded Systems Institute, Eindhoven, The Netherlands},

5974

  year = {2007},

5975

  editor = {Jan Tretmans},

5976

  owner = {harald},

5977

  timestamp = {2009.09.18}

5978

5979

5980

@PROCEEDINGS{Uyar2006,

5981

  title = {Testing of Communicating Systems, 18th IFIP TC6/WG6.1 International

5982

	Conference, TestCom 2006, New York, NY, USA, May 16-18, 2006, Proceedings},

5983

  year = {2006},

5984

  editor = {M. {\"U}mit Uyar and Ali Y. Duale and Mariusz A. Fecko},

5985

  volume = {3964},

5986

  series = {Lecture Notes in Computer Science},

5987

  publisher = {Springer},

5988

  bibsource = {DBLP, http://dblp.uni-trier.de},

5989

  booktitle = {TestCom},

5990

  isbn = {3-540-34184-6},

5991

  owner = {harald},

5992

  timestamp = {2009.09.18}

5993

5994

5995

@PROCEEDINGS{Wermelinger2005,

5996

  title = {Proceedings of the 10th European Software Engineering Conference

5997

	held jointly with 13th ACM SIGSOFT International Symposium on Foundations

5998

	of Software Engineering, 2005, Lisbon, Portugal, September 5-9, 2005},

5999

  year = {2005},

6000

  editor = {Michel Wermelinger and Harald Gall},

6001

  publisher = {ACM},

6002

  bibsource = {DBLP, http://dblp.uni-trier.de},

6003

  booktitle = {ESEC/SIGSOFT FSE},

6004

  isbn = {1-59593-014-0},

6005

  owner = {harald},

6006

  timestamp = {2009.09.18}

6007

6008

6009

@MISC{,

6010

  title = {{T-VEC Tester for Simulink homepage}},

6011

  howpublished = {\url{http://www.t-vec.com/solutions/simulink.php}},

6012

  note = {(checked Aug 10, 2009)},

6013

  key = {t-vec-homepage},

6014

  owner = {harald},

6015

  timestamp = {2009.09.18}

6016

6017

6018

@MISC{,

6019

  title = {{Simulink Design Verifier homepage}},

6020

  howpublished = {\url{http://www.mathworks.com/products/sldesignverifier/}},

6021

  note = {(checked Aug 10, 2009)},

6022

  key = {simulink-design-verifier-homepage},

6023

  owner = {harald},

6024

  timestamp = {2009.09.18}

6025

6026

6027

@MISC{,

6028

  title = {{SCADE} product page},

6029

  howpublished = {\url{http://www.esterel-technologies.com/products/scade-suite/}},

6030

  note = {(checked Aug 10, 2009)},

6031

  key = {scade-homepage},

6032

  owner = {harald},

6033

  timestamp = {2009.09.18}

6034

6035

6036

@MISC{,

6037

  title = {{MaTeLo Product Page}},

6038

  howpublished = {\url{http://www.all4tec.net/index.php/All4tec/matelo-product.html}},

6039

  note = {(checked Aug 5, 2009)},

6040

  key = {MaTeLo},

6041

  owner = {harald},

6042

  timestamp = {2009.09.18}

6043

6044

6045

@MISC{,

6046

  title = {{BEACON Tester homepage}},

6047

  howpublished = {\url{http://www.adi.com/products\_be\_bss\_te.htm}},

6048

  note = {(checked Aug 10, 2009)},

6049

  key = {beacon-homepage},

6050

  owner = {harald},

6051

  timestamp = {2009.09.18}

6052

6053

6054

@MISC{,

6055

  title = {{IBM Rational Tau product page}},

6056

  howpublished = {\url{http://www.telelogic.com/products/tau/}},

6057

  note = {(checked August 5, 2009)},

6058

  key = {tautoolset},

6059

  owner = {harald},

6060

  timestamp = {2009.09.18}

6061

6062

6063

@PROCEEDINGS{2007,

6064

  title = {2007 IEEE Symposium on Security and Privacy (S{\&}P 2007), 20-23

6065

	May 2007, Oakland, California, USA},

6066

  year = {2007},

6067

  publisher = {IEEE Computer Society},

6068

  bibsource = {DBLP, http://dblp.uni-trier.de},

6069

  booktitle = {IEEE Symposium on Security and Privacy},

6070

  key = {IEEE},

6071

  owner = {harald},

6072

  timestamp = {2009.09.18}

6073

6074

6075

@MISC{2006,

6076

  title = {Standard ECMA--335, Common Language Infrastructure (CLI)},

6077

  month = {June},

6078

  year = {2006},

6079

  key = {ECMA},

6080

  owner = {harald},

6081

  timestamp = {2009.09.18}

6082

6083

6084

@PROCEEDINGS{2006a,

6085

  title = {Proceedings of the Canadian Conference on Electrical and Computer

6086

	Engineering, CCECE 2007, May 7, 10, 2006, Ottawa Congress Centre,

6087

	Ottawa, Canada},

6088

  year = {2006},

6089

  publisher = {IEEE},

6090

  bibsource = {DBLP, http://dblp.uni-trier.de},

6091

  booktitle = {CCECE},

6092

  owner = {harald},

6093

  timestamp = {2009.09.18}

6094

6095

6096

@PROCEEDINGS{2004,

6097

  title = {10th IEEE Real-Time and Embedded Technology and Applications Symposium

6098

	(RTAS 2004), 25-28 May 2004, Toronto, Canada},

6099

  year = {2004},

6100

  publisher = {IEEE Computer Society},

6101

  bibsource = {DBLP, http://dblp.uni-trier.de},

6102

  booktitle = {IEEE Real-Time and Embedded Technology and Applications Symposium},

6103

  isbn = {0-7695-2148-7},

6104

  owner = {harald},

6105

  timestamp = {2009.09.18}

6106

6107

6108

@PROCEEDINGS{2003,

6109

  title = {3rd International Conference on Quality Software (QSIC 2003), 6-7

6110

	November 2003, Dallas, TX, USA},

6111

  year = {2003},

6112

  publisher = {IEEE Computer Society},

6113

  bibsource = {DBLP, http://dblp.uni-trier.de},

6114

  booktitle = {QSIC},

6115

  isbn = {0-7695-2015-4},

6116

  owner = {harald},

6117

  timestamp = {2009.09.18}

6118

6119

6120

@PROCEEDINGS{2002,

6121

  title = {8th International Conference on Engineering of Complex Computer Systems

6122

	(ICECCS 2002), 2-4 December 2002, Greenbelt, MD, USA},

6123

  year = {2002},

6124

  publisher = {IEEE Computer Society},

6125

  bibsource = {DBLP, http://dblp.uni-trier.de},

6126

  booktitle = {ICECCS},

6127

  isbn = {0-7695-1757-9},

6128

  owner = {harald},

6129

  timestamp = {2009.09.18}

6130

6131

6132

@PROCEEDINGS{1998,

6133

  title = {2nd Workshop on Industrial-Strength Formal Specification Techniques

6134

	(WIFT '98), October 20-23, 1998, Boca Raton, FL, USA},

6135

  year = {1998},

6136

  publisher = {IEEE Computer Society},

6137

  bibsource = {DBLP, http://dblp.uni-trier.de},

6138

  booktitle = {WIFT},

6139

  isbn = {0-7695-0081-1},

6140

  owner = {harald},

6141

  timestamp = {2009.09.18}

6142

6143

6144

@comment{jabref-meta: selector_publisher:}

6145

6146

@comment{jabref-meta: selector_author:}

6147

6148

@comment{jabref-meta: selector_journal:}

6149

6150

@comment{jabref-meta: selector_keywords:}

Project

General

Profile

OoasTools

root / branches / compiler / cSharp / ooasCompiler / doc / papers.bib @ 3