-
Notifications
You must be signed in to change notification settings - Fork 19
/
Copy pathcofi-ann.bib
2990 lines (2798 loc) · 145 KB
/
cofi-ann.bib
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
cofi.bib
BibTeX data for publications on:
* CoFI: The Common Framework Initiative
for algebraic specification and development
* CASL: The Common Algebraic Specification Language
The companion file cofi-abbr.bib provides abbreviated output.
Maintained by Peter D. Mosses <pdmosses at brics.dk>
Last updated: 11 Jan 2004
See <http://www.cofi.info/Bibliography> for updates.
****************************************************************
JOURNALS:
@String{acmcs = "ACM Computing Surveys"}
@String{acta = "Acta Informatica"}
@String{cacm = "Communications of the ACM"}
@String{cai = "Computing and Informatics"}
@String{eatcs = "Bulletin of the EATCS"}
@String{fac = "Formal Aspects of Computing"}
@String{ieeese = "IEEE Transactions on Software Engineering"}
@String{ieeetc = "IEEE Transactions on Computers"}
@String{ipl = "Information Processing Letters"}
@String{jacm = "Journal of the ACM"}
@String{jcss = "Journal of Computer and System Sciences"}
@String{jlc = "Journal of Logic and Computation"}
@String{njc = "Nordic Journal of Computing"}
@String{scp = "Science of Computer Programming"}
@String{sicomp = "SIAM Journal on Computing"}
@String{tocs = "ACM Transactions on Computer Systems"}
@String{toplas = "ACM Transactions on Programming Languages and
Systems"}
@String{tcs = "Theoretical Computer Science"}
@String{spe = "Software: Practice and Experience"}
SERIES, to be concatenated with the VOLUME NUMBER:
@String{amast = "AMAST Series in Computing Vol.~"}
@String{entcs = "ENTCS Vol.~"}
@String{facit = "FACIT (Formal Approaches to Computing and Information
Technology)"}
@String{lncs = "LNCS Vol.~"}
E.g. series = lncs # "1234", and OMIT volume = ...
TYPES:
@String{chap = "Chapter"}
@String{tech-rep = "Technical Report"}
PUBLISHERS:
@String{pub-acm = "ACM Press"}
@String{pub-bcs = "British Computer Society"}
@String{pub-cup = "Cambridge University Press"}
@String{pub-elsevier = "Elsevier"}
@String{pub-ieee = "IEEE Press"}
@String{pub-ios = "IOS Press"}
@String{pub-kluwer = "Kluwer Academic Publishers Group"}
@String{pub-oxford = "Oxford University Press"}
@String{pub-prentice-hall = "Prentice-Hall"}
@String{pub-springer = "Springer"}
@String{pub-world-sci = "World Scientific"}
****************************************************************
REFERENCES:
* The tag format is generally Author:YYYY:TTT, where:
* - Author is surname of first author
* - YYYY is the 4-digit year of PUBLICATION
* - TTT is usually the initial letters of
* the first 3 SIGNIFICANT words in the title
@InProceedings{Ancona:2000:ECL,
author = "Davide Ancona and Maura Cerioli and Elena Zucca",
title = "Extending \textsc{Casl} by Late Binding",
pages = "53--72",
crossref = "WADT-99",
URL = "ftp://ftp.disi.unige.it/pub/person/AnconaD/DISI-TR-99-14.ps.gz",
abstract = "We define an extension of \textsc{Casl}, the standard
language for algebraic specification, with a late
binding mechanism. More precisely, we introduce a
special kind of functions called methods, for which,
differently to what happens for usual functions,
overloading resolution is delayed at evaluation time
and not required to be conservative. The extension
consists, at the semantic level, in the definition of
an institution LBInst supporting late binding which is
defined on top of the standard subsorted institution of
\textsc{Casl} and, at the linguistic level, in the
enrichment of the \textsc{Casl} language with
appropriate constructs for dealing with methods. In
addition to this, we propose a further enrichment of
the \textsc{Casl} language which is made possible by
introduction of late binding, that is a mechanism for
``inheriting'' axioms from a supersort with the
possibility of overriding them. The aim is to obtain
advantages in terms of reuse of specifications similar
to those obtained by inheritance in object-oriented
programming languages.",
annote = "Proposes an extension of \textsc{Casl} with methods,
which are special functions s.t.\ overloading
resolution for them is delayed to evaluation time and
is not required to be conservative.",
}
@InProceedings{Aspinall:2002:FSC,
author = "David Aspinall and Donald Sannella",
title = "From Specifications to Code in \textsc{Casl}",
pages = "1--14",
crossref = "AMAST-2002",
URL = "http://www.dcs.ed.ac.uk/home/dts/pub/amast2002.pdf",
abstract = "The status of the Common Framework Initiative
(\textsc{CoFI}) and the Common Algebraic Specification
Language (\textsc{Casl}) are briefly presented. One
important outstanding point concerns the relationship
between \textsc{Casl} and programming languages; making
a proper connection is obviously central to the use of
\textsc{Casl} specifications for software specification
and development. Some of the issues involved in making
this connection are discussed.",
annote = "Discusses the relationship between \textsc{Casl} and
programming languages.",
}
@InProceedings{Astesiano:1998:UHM,
author = "Egidio Astesiano and Gianna Reggio",
title = "{UML} as Heterogeneous Multiview Notation: Strategies
for a Formal Foundation",
editor = "L. Andrade and A. Moreira and A. Deshpande and S.
Kent",
booktitle = "Proceedings of the OOPSLA'98 Workshop on Formalizing
UML. Why? How?",
year = "1998",
publisher = pub-acm,
annote =
"The paper presents some initial ideas about the
formalization of the UML."
}
@InCollection{Astesiano:1999:ASC,
author = "Egidio Astesiano and Manfred Broy and Gianna Reggio",
title = "Algebraic Specification of Concurrent Systems",
chapter = "13",
type = chap,
crossref = "IFIP-AFS",
annote = "Presents a survey of the algebraic methods
for the specification of
concurrent systems, using a common
simple example,
and classifying them in four kinds."
}
@InProceedings{Astesiano:2000:PDC,
author = "Egidio Astesiano and Maura Cerioli and Gianna Reggio",
title = "Plugging Data Constructs into Paradigm-Specific
Languages: Towards an Application to {UML}",
pages = "273--292",
crossref = "AMAST-2000",
URL = "ftp://ftp.disi.unige.it/pub/person/ReggioG/AstesianoEtAll00a.ps",
abstract = "We are interested in the composition of languages, in
particular a data description language and a
paradigm-specific language, from a pragmatic point of
view. Roughly speaking our goal is the description of
languages in a component-based style, focussing on the
data definition component. The proposed approach is to
substitute the constructs dealing with data from the
``data'' language for the constructs describing data
that are not specific to the particular paradigm of the
``paradigm-specific'' language in a way that syntax,
semantics as well as methodologies of the two
components are preserved. We illustrate our proposal on
a toy example: using the algebraic specification
language \textsc{Casl}, as data language, and a
``pre-post'' condition logic à la Hoare, as the
paradigm specific one. A more interesting application
of our technique is fully worked out elsewhere and the
first step towards an application to UML, that is an
analysis of UML from the data viewpoint, following the
guidelines given here, is sketched at the end.",
annote = "Presents an approach for the composition of languages, in
particular a data description language and a
paradigm-specific language, exemplified by sketching how
to combine UML and a data language."
}
@Article{Astesiano:2001:LTL,
author = "Egidio Astesiano and Gianna Reggio",
title = "{Labelled Transition Logic}: An Outline",
journal = acta,
year = "2001",
volume = "37",
number = "11--12",
OPTpublisher = pub-springer,
abstract = "In the last ten years we have developed and
experimented in a series of projects, including
industry test cases, a method for the specification of
reactive/distributed/\ldots\ systems both at the
requirement and at the design level. We present here in
outline its main technical features, providing
appropriate references for more detailed presentations
of single aspects and applications. The overall main
feature of the method is its logical (algebraic)
character, because it extends to labelled transition
systems the logical/algebraic specification method of
abstract data types; moreover systems are viewed as
data within first-order structures called
LT-structures. Some advantages of the approach are the
full integration of the specification of static data
and of dynamic systems, which includes by free
higher-order concurrency, and the exploitation of
well-explored classical techniques in many respects,
including implementation and tools.",
annote = "Outlines a logical (algebraic) method for the
specification of reactive/distributed systems both at
the requirement and at the design level, providing
references for detailed presentations of single aspects
and applications.",
}
@Article{Astesiano:2002:CASL,
author = "Egidio Astesiano and Michel Bidoit and H{\'e}l{\`e}ne
Kirchner and Bernd Krieg-Br{\"u}ckner and Peter D.
Mosses and Donald Sannella and Andrzej Tarlecki",
title = "\textsc{Casl}: The {Common Algebraic Specification
Language}",
journal = tcs,
year = "2002",
volume = "286",
number = "2",
pages = "153--196",
abstract = "The Common Algebraic Specification Language
(\textsc{Casl}) is an expressive language for the
formal specification of functional requirements and
modular design of software. It has been designed by
COFI, the international Common Framework Initiative for
algebraic specification and development. It is based on
a critical selection of features that have already been
explored in various contexts, including subsorts,
partial functions, first-order logic, and structured
and architectural specifications. \textsc{Casl} should
facilitate interoperability of many existing algebraic
prototyping and verification tools. This paper gives an
overview of the \textsc{Casl} design. The major issues
that had to be resolved in the design process are
indicated, and all the main concepts and constructs of
\textsc{Casl} are briefly explained and illustrated the
reader is referred to the \textsc{Casl} Language
Summary for further details. Some familiarity with the
fundamental concepts of algebraic specification would
be advantageous.",
annote = "Gives an overview of the \textsc{Casl} design,
indicating major issues, and explaining main concepts
and constructs. Compares \textsc{Casl} to some other
major algebraic specification languages.",
}
@InProceedings{Autexier:2000:TEF,
author = "Serge Autexier and Dieter Hutter and Heiko Mantel and
Axel Schairer",
title = "Towards an Evolutionary Formal Software-Development
Using \textsc{Casl}",
pages = "73--88",
crossref = "WADT-99",
annote = "Defines a translation of a subset of CASL into the
notion of development graphs, in order to maintain
evolving \textsc{Casl} specifications.",
}
@InProceedings{Autexier:2002:DGM,
author = "Serge Autexier and Dieter Hutter and Till Mossakowski
and Axel Schairer",
title = "The Development Graph Manager \textsc{Maya} (System
Description)",
crossref = "AMAST-2002",
pages = "495--502",
annote = "Explains the \textsc{Maya} system, which maintains
structured specifications and their proofs with the
help of development graphs.",
}
@InProceedings{Autexier:2002:IHD,
author = "Serge Autexier and Till Mossakowski",
title = "Integrating \textsc{Hol-Casl} into the Development
Graph Manager \textsc{Maya}",
pages = "2--17",
crossref = "FROCOS-2002",
abstract = "For the recently developed specification language
\textsc{Casl}, there exist two different kinds of proof
support: while \textsc{Hol-Casl} has its strength in
proofs about specifications in-the-small, MAYA has been
designed for management of proofs in (\textsc{Casl})
specifications in-the-large, within an evolutionary
formal software development process involving changes
of specifications. In this work, we discuss our
integration of \textsc{Hol-Casl} and MAYA into a
powerful system providing tool support for
\textsc{Casl}, which will also serve as a basis for the
integration of further proof tools.",
annote = "\textsc{Maya} provides management of proofs for
structured specifications; \textsc{Hol-Casl} is a
prover for \textsc{Casl} basic specifications. Here,
these two are combined",
}
@InProceedings{Baumeister:2000:ASC,
author = "Hubert Baumeister and Didier Bert",
title = "Algebraic Specification in \textsc{Casl}",
crossref = "FACIT-2000",
chapter = "12",
type = chap,
pages = "209--224",
URL = "http://www.informatik.uni-muenchen.de/~baumeist/CoFI/case/pubs/casl-case.ps.gz",
annote = "Explains the basic features of \textsc{Casl}
specifications using the warehouse case study.",
}
@InProceedings{Baumeister:2000:RAD,
author = "Hubert Baumeister",
title = "Relating Abstract Datatypes and {Z}-Schemata",
pages = "366--382",
crossref = "WADT-99",
URL = "http://www.informatik.uni-muenchen.de/~baumeist/publications/wadt99.pdf",
abstract = "In this paper we investigate formally the relationship
between the notion of abstract datatypes in an
arbitrary institution, found in algebraic specification
languages like Clear, ASL and \textsc{Casl}; and the
notion of schemata from the model-oriented
specification language Z. To this end the institution S
of the logic underlying Z is defined and a translation
of Z-schemata to abstract datatypes over S is given.
The notion of a schema is internal to the logic of Z
and thus specification techniques of Z relying on the
notion of a schema can only be applied in the context
of Z. By translating Z-schemata to abstract datatypes
these specification techniques can be transformed to
specification techniques using abstract datatypes.
Since the notion of abstract datatypes is institution
independent, this results in a separation of these
specification techniques from the specification
language Z and allows them to be applied in the context
of other, e.g. algebraic, specification languages.",
annote = "Defines an institution for the logic underlying Z.
Shows a translation of Z-schemata to abstract datatypes
over that institution.",
}
@InProceedings{Baumeister:2000:SBE,
author = "Hubert Baumeister and Alexandre V. Zamulin",
title = "State-Based Extension of \textsc{Casl}",
pages = "3--24",
crossref = "IFM-2000",
URL = "http://www.informatik.uni-muenchen.de/~baumeist/ifm2000.ps.gz",
abstract = "A state-based extension of the algebraic specification
language \textsc{Casl} is presented. It permits the
specification of the static part of a complex dynamic
system by means of \textsc{Casl} and the dynamic part
by means of the facilities described in the paper. The
dynamic system is defined as possessing a number of
states and a number of operations (procedures) for
transforming one state into another. Each state
possesses one and the same static part specified by
\textsc{Casl} and a varying part specified by
additional tools. The varying part includes dynamic
sorts/functions/predicates and dependent
functions/predicates. The dependent
functions/predicates are specified by formulae using
the names of the dynamic functions/predicates so that
each time one of the last ones is updated the
corresponding former ones are also updated. The updates
of the dynamic entities are produced by procedures
which are specified by means of preconditions,
postconditions and dynamic equations.",
annote = "Presents an extension of \textsc{Casl} for writing
model-oriented specifications. The extension is based
on the state-as-algebra approach.",
}
@InCollection{Baumeister:2004:CASL-Semantics,
author = "Hubert Baumeister and Maura Cerioli and Anne
Haxthausen and Till Mossakowski and Peter D. Mosses and
Donald Sannella and Andrzej Tarlecki",
title = "\textsc{Casl} Semantics",
chapter = "III",
type = "Part",
note = "Edited by D. Sannella and A. Tarlecki",
crossref = "CASL-RM",
annote = "Presents the complete semantics of \textsc{Casl} in
natural semantics style.",
}
@InProceedings{Bert:2000:ASO,
author = "Didier Bert and S. {Lo Presti}",
title = "Algebraic Specification of Operator-based Multimedia
Scenarios",
pages = "383--400",
crossref = "WADT-99",
annote = "Presents a set of algebraic operators in CASL to
create complex scenarios. Provides a semantics in a
temporal model and shows how to derive some properties
of the scenarios.",
}
@InProceedings{Bidoit:1998:ASC,
author = "Michel Bidoit and Donald Sannella and Andrzej
Tarlecki",
title = "Architectural Specifications in \textsc{Casl}",
pages = "341--357",
crossref = "AMAST-98",
note = "An extended and improved version is
\citeann{ann-Bidoit:2002:ASC}",
annote = "Motivates and presents \textsc{Casl} architectural
specifications.",
}
@Article{Bidoit:2002:ASC,
author = "Michel Bidoit and Donald Sannella and Andrzej
Tarlecki",
title = "Architectural Specifications in \textsc{Casl}",
journal = fac,
year = "2002",
volume = "13",
pages = "252--273",
URL = "http://www.dcs.ed.ac.uk/home/dts/pub/archs.pdf",
abstract = "One of the most novel features of \textsc{Casl}, the
Common Algebraic Specification Language, is the
provision of so-called architectural specifications for
describing the modular structure of software systems. A
brief discussion of refinement of \textsc{Casl}
specifications provides the setting for a presentation
of the rationale behind architectural specifications.
This is followed by some details of the features
provided in \textsc{Casl} for architectural
specifications, hints concerning their semantics, and
simple results justifying their usefulness in the
development process.",
annote = "Gives an informal motivation for and presentation of
\textsc{Casl} architectural specifications, with hints
on their semantics and use in the development
process.",
}
@InProceedings{Bidoit:2002:GDL,
author = "Michel Bidoit and Donald Sannella and Andrzej
Tarlecki",
title = "Global Development via Local Observational
Construction Steps",
pages = "1--24",
crossref = "MFCS-2002",
abstract = "The way that refinement of individual ``local''
components of a specification relates to development of
a ``global'' system from a specification of
requirements is explored. Observational interpretation
of specifications and refinements add expressive power
and flexibility while bringing in some subtle problems.
The results are instantiated in the context of
\textsc{Casl} architectural specifications.",
annote = "Studies development steps that apply local
constructions in a global context, and gives the
semantics of a version of \textsc{Casl} architectural
specifications, including their observational
interpretation.",
}
@Book{Bidoit:2004:CASL-UM,
author = "Michel Bidoit and Peter D. Mosses",
title = "\textsc{Casl} User Manual",
publisher = pub-springer,
year = "2004",
series = lncs # "2900 (IFIP Series)",
note = "With chapters by Till Mossakowski, Donald Sannella,
and Andrzej Tarlecki",
annote = "Illustrates and discusses how to write \textsc{Casl}
specifications, with additional chapters on
foundations, tools, and libraries, a realistic case
study, and a quick-reference overview of
\textsc{Casl}.",
note = {Free online version available at \url{http://www.cofi.info}},
}
@InProceedings{Bidoit:2004:CFS,
author = "Michel Bidoit and Donald Sannella and Andrzej
Tarlecki",
title = "Toward Component-Oriented Formal Software Development:
An Algebraic Approach",
booktitle = "Radical Innovations of Software and Systems
Engineering in the Future, Proc. 9th Monterey Software
Engineering Workshop, Venice, Italy, Sep. 2002",
editor = "M. Wirsing and A. Knapp and S. Balsamo",
missingpages = "not known yet",
series = lncs # "2941",
year = "2004",
publisher = pub-springer,
URL = "http://www.dcs.ed.ac.uk/home/dts/pub/monterey.pdf",
abstract = "Component based design and development of software is
one of the most challenging issues in software
engineering. In this paper, we adopt a somewhat
simplified view of software components and discuss how
they can be conveniently modeled in a framework that
provides a modular approach to formal software
development by means of stepwise refinements. In
particular we take into account an observational
interpretation of requirements specifications and study
its impact on the definition of the semantics of
specifications of (parametrized) components. Our study
is carried out in the context of \textsc{Casl}
architectural specifications.",
annote = "Provides a light-weight introduction to
\citeann{ann-Bidoit:2002:GDL}, with an illustrative example.",
}
@Article{Borzyszkowski:2000:GIC,
author = "Tomasz Borzyszkowski",
title = "Generalized Interpolation in \textsc{Casl}",
journal = ipl,
year = "2000",
volume = "76",
pages = "19--24",
URL = "http://delta.math.univ.gda.pl/~tomek/papers/ipl00.pdf",
abstract = "In this paper we consider the partial many-sorted
first-order logic and its extension to the subsorted
partial many-sorted first-order logic
that underly the \textsc{Casl} specification formalism.
First we present counterexamples showing that
the generalization of the Craig Interpolation Property
does not hold for these logics in general
(i.e., with respect to arbitrary signature morphisms).
Then we formulate conditions under which
the generalization of the Craig Interpolation Property
holds for the first logic.",
annote = "Gives a proof of the Craig Interpolation Property for
the partial many-sorted first-order logic, underlying \textsc{Casl}.
This property is crucial for results presented
in~\cite{ann-Borzyszkowski:2002:LSS}.",
}
@InProceedings{Borzyszkowski:2000:HOL,
author = "Tomasz Borzyszkowski",
title = "Higher-Order Logic and Theorem Proving for Structured
Specifications",
pages = "401--418",
crossref = "WADT-99",
URL = "http://delta.math.univ.gda.pl/~tomek/papers/wadt99.pdf",
abstract = "In this paper we present the higher-order
logic used in theorem-provers like
the HOL system or Isabelle HOL logic
as an institution. Then we show that for maps
of institutions into HOL that satisfy certain
technical conditions we can reuse the proof
system of the higher-order logic to reason
about structured specifications built over
the institutions mapped into HOL.
We also show some maps of institutions
underlying the \textsc{Casl} specification formalism
into HOL that satisfy conditions needed for
reusing proof systems.",
annote = "Formulates conditions under which we can reuse
the HOL logic to reason about structured specifications
built over institutions mapped into HOL. It works also for
the \emph{structured part} of \textsc{Casl}.",
}
@Article{Borzyszkowski:2002:LSS,
author = "Tomasz Borzyszkowski",
title = "Logical systems for structured specifications",
journal = tcs,
year = "2002",
volume = "286",
pages = "197--245",
URL = "http://delta.math.univ.gda.pl/~tomek/papers/tcs02.pdf",
abstract = "We study proof systems for reasoning about
logical consequences and refinement of structured
specifications, based on similar
systems proposed earlier in the literature.
Following Goguen and Burstall, the notion of
an underlying logical system over which we build
specifications is formalized as an institution and
extended to a more general notion, called
$(\cal{D},\cal{T})$-institution.
We show that under simple assumptions
(essentially: amalgamation and interpolation)
the proposed proof systems are sound and complete.
The completeness proofs are inspired by proofs due
to M.~V.~Cengarle for specifications in first-order
logic and the logical systems for reasoning about them.
We then propose a methodology for reusing proof systems
built over institutions rich enough to satisfy
the properties required for the completeness results
for specifications built over poorer institutions
where these properties need not hold.",
annote = "Presents completeness results for proof
systems for structured specifications.
Also introduces a methodology for reusing complete proof systems
for systems that are not complete.",
}
@InProceedings{Brand:2000:DPT,
author = "Mark G. J. {\iffalse{brandscheerder}\fi}{van den}
Brand and Jeroen Scheerder",
author-alpha = "Mark G. J. {\iffalse{bs}\fi}{van den} Brand and Jeroen
Scheerder",
title = "Development of Parsing Tools for \textsc{Casl} using
Generic Language Technology",
pages = "89--105",
crossref = "WADT-99",
abstract = "An environment for the Common Algebraic Specification
Language CASL consists of several independent tools. A
number of CASL tools have been built using the
algebraic specification formalism {\sc Asf+Sdf} and the
{\sc Asf+Sdf} Meta-Environment. CASL supports
user-defined syntax which non-trivial to process: {\sc
Asf+Sdf} offers a powerful parsing technology
(Generalized LR). Its interactive development
environment facilitates rapid prototyping complemented
bt early detection and correction of errors. A number
of core technologies developed for the {\sc Asf+Sdf}
Meta-Environment can be reused in the context of CASL.
Furthermore, an instantiaion of a generic format
developed for the representation of {\sc Asf+Sdf}
specifications and terms provides a CASL-specific
exchange format.",
annote = "Describes the architecture of a \textsc{Casl} parser
based on the SGLR parsing technology developed for
\textsc{Asf+Sdf}, and discusses the mapping to abstract
syntax trees represented as ATerms.",
}
@Article{Brand:2000:EAT,
author = "Mark G. J. {\iffalse{brandjongklintolivier}\fi}{van
den} Brand and Hayco A. {\iffalse{}\fi}{de} Jong and
Paul Klint and Pieter A. Olivier",
author-alpha = "Mark G. J. {\iffalse{bjko}\fi}{van den} Brand and
Hayco A. {\iffalse{}\fi}{de} Jong and Paul Klint and
Pieter A. Olivier",
title = "Efficient Annotated Terms",
journal = spe,
year = "2000",
volume = "30",
number = "3",
pages = "259--291",
abstract =
"How do distributed applications exchange tree-like data structures? We
introduce the abstract data type of \emph{Annotated Terms}
(\emph{ATerms}) and discuss their design, implementation and
application. A comprehensive procedural interface enables
creation and manipulation of ATerms in C or Java.
The ATerm implementation is based on maximal subterm
sharing and automatic garbage collection.
A binary exchange format for the
concise representation of ATerms (sharing preserved) allows the
fast exchange of ATerms between applications. In a typical
application---parse trees which contain considerable redundant
information---less than 2 \emph{bytes} are needed to represent
a node in memory,
and less than 2 \emph{bits} are needed to represent it in binary format.
The implementation of ATerms scales up to the manipulation
of ATerms in the giga-byte range.",
annote = "Describes an efficient and generic representation of
tree-like data structures, and reports on several case studies,
including the abstract syntax of \textsc{Casl}.",
}
@Book{COMPASS:1997,
editor = "Maura Cerioli and Martin Gogolla and H{\'e}l{\`e}ne
Kirchner and Bernd Krieg-Br{\"u}ckner and Zhenyu Qian
and Markus Wolf",
title = "Algebraic System Specification and Development: Survey
and Annotated Bibliography",
publisher = "Shaker",
year = "1998",
series = "BISS Monographs",
edition = "2nd",
annote = "Provides an overview of the state of the art in algebraic
specification at the end of the 90's, with a comprehensive bibliography.
Discusses semantics, structuring constructs, specific algebraic
paradigms, methodology issues, and existing tools.",
}
@InProceedings{Cerioli:1997:PSP,
author = "Maura Cerioli and Anne Haxthausen and Bernd
Krieg-Br{\"u}ckner and Till Mossakowski",
title = "Permissive Subsorted Partial Logic in \textsc{Casl}",
pages = "91--107",
crossref = "AMAST-97",
abstract = "This paper presents a permissive subsorted partial
logic used in the CoFI Algebraic Specification
Language. In contrast to other order-sorted logics,
subsorting is not modeled by set inclusions, but by
injective embeddings allowing for more general models
in which subtypes can have different data type
representations. Furthermore, there are no restrictions
like monotonicity, regularity or local filtration on
signatures at all. Instead, the use of overloaded
functions and predicates in formulae is required to be
sufficiently disambiguated, such that all parses have
the same semantics. An overload resolution algorithm is
sketched.",
annote = "Presents the permissive subsorted partial logic used
in the \textsc{Casl} semantics.",
}
@InCollection{Cerioli:1999:TEP,
author = "Maura Cerioli and Till Mossakowski and Horst Reichel",
title = "From Total Equational to Partial First-Order Logic",
chapter = "3",
crossref = "IFIP-AFS",
abstract = "The focus of this chapter is the incremental
presentation of partial first-order logic, seen as a
powerful framework where the specification of most data
types can be directly represented in the most natural
way. Both model theory and logical deduction are fully
described. Alternatives to partiality, like (variants
of) error algebras and order-sortedness, are also
discussed, emphasizing their uses and limitations.
Moreover, both the total and the partial (positive)
conditional fragments are investigated in detail, and
in particular the existence of initial (free) models
for such restricted logical paradigms is proved.
Finally some more powerful algebraic frameworks are
sketched.",
annote = "Presents partial first-order logic, both model theory
and logical deduction. Compares partial specifications
to error algebras and order-sortedness.",
}
@TechReport{Choppy:1999:UCS,
author = "Christine Choppy and Gianna Reggio",
title = "Using \textsc{Casl} to Specify the Requirements and
the Design: {A} Problem Specific Approach -- Complete
Version",
institution = "Univ. of Genova",
year = "1999",
type = tech-rep,
number = "DISI-TR-99-33",
URL = "ftp://ftp.disi.unige.it/person/ReggioG/ChoppyReggio99a.ps",
note = "This is an extended version of \citeann{ann-Choppy:2000:UCS},
including complete case studies.",
annote = "Shows how formal specification skeletons may be
associated with the structuring concepts provided by M.
Jackson's Problem Frames, used to provide a first gross
structure and characterization of the system under
study.",
}
@InProceedings{Choppy:2000:UCS,
author = "Christine Choppy and Gianna Reggio",
title = "Using \textsc{Casl} to Specify the Requirements and
the Design: {A} Problem Specific Approach",
pages = "104--123",
crossref = "WADT-99",
URL = "ftp://ftp.disi.unige.it/person/ReggioG/ChoppyReggio99a.ps",
abstract = "In his 1995 book, M. Jackson introduces the concept of
\textit{problem frame} to describe specific classes of
problems, to help in the specification and design of
systems, and also to provide a framework for
reusability. He thus identifies some particular frames,
such as the translation frame (e.g., a compiler), the
information system frame, the control frame (or
reactive system frame), \ldots . Each frame is
described along three viewpoints that are application
domains, requirements, and design. Our aim is to use
\textsc{Casl} (or possibly a sublanguage or an
extension of \textsc{Casl} if and when appropriate) to
formally specify the requirements and the design of
particular classes of problems (``problem frames'').
This goal is related to methodology issues for
\textsc{Casl}, that are here addressed in a more
specific way, having in mind some particular problem
frame, i.e., a class of systems. It is hoped that this
will provide both a help in using, in a really
effective way, \textsc{Casl} for system specifications,
a link with approaches that are currently used in the
industry, and a framework for the reusability. This
approach is illustrated with some case studies, e.g.,
the information system frame is illustrated with the
invoice system.",
note = "An extended version is provided in
\citeann{ann-Choppy:1999:UCS}",
annote = "Shows how formal specification skeletons may be
associated with the structuring concepts provided by M.
Jackson's Problem Frames, used to provide a first gross
structure and characterization of the system under
study.",
}
@TechReport{Choppy:2003:TFG,
author = "Christine Choppy and Gianna Reggio",
title = "Towards a Formally Grounded Software Development
Method",
year = "2003",
institution = "Univ. of Genova",
type = tech-rep,
number = "DISI-TR-03-35",
URL = "ftp://ftp.disi.unige.it/person/ReggioG/ChoppyReggio03a.pdf",
url-ps = "ftp://ftp.disi.unige.it/person/ReggioG/ChoppyReggio03a.ps",
month = aug,
abstract = "One of the goals of software engineering is to provide
what is necessary to write relevant, legible, useful
descriptions of the systems to be developed, which will
be the basis of successful developments. This goal was
addressed both from informal approaches (providing in
particular visual languages) and formal ones (providing
a formal sound semantic basis). Informal approaches are
often driven by a software development method, and
while formal approaches sometimes provide a user
method, it is usually aimed at helping to use the
proposed formalism/language when writing a
specification. Our goal here is to provide a companion
method that helps the user to understand the system to
be developed, and to write the corresponding formal
specifications. We also aim at supporting visual
presentations of formal specifications, so as to ``make
the best of both formal and informal worlds''. We
developed this method for the (logical-algebraic)
specification languages \textsc{Casl} (Common Algebraic
Specification Language, developed within the joint
initiative CoFI) and for an extension for dynamic
systems \textsc{Cas-Ltl}, and we believe it is general
enough to be adapted to other paradigms. Another
challenge is that a method that is too general does not
encompass the different kinds of systems to be studied,
while too many different specialized methods and
paradigms result in partial views that may be difficult
to integrate in a single global one. We deal with this
issue by providing a limited number of instances of our
method, fitted for three different kinds of software
items and two specification approaches, while keeping a
common ``meta''-structure and way of thinking. More
precisely, we consider here that a software item may be
a simple dynamic system, a structured dynamic system,
or a data structure. We also support both
property-oriented (axiomatic) and model-oriented
(constructive) specifications. We are thus providing
support for the ``building-bricks'' tasks of
specifying/modelling software artifacts that in our
experience are needed for the development process. Our
approach is illustrated with a lift case study, it was
also used with other large case studies, and when used
on projects by students yielded homogeneous results.
Let us note that it may be used either as itself, e.g.,
for requirements specification, or in combination with
structuring concepts such as the Jackson's problem
frames.",
annote = "Presents guidelines for writing (and meanwhile
understanding) descriptions/specifications, both in
property-oriented and model-oriented styles. Provides
visual descriptions, and formal specifications in
\textsc{Casl-Ltl}.",
}
@TechReport{Choppy:2003:IUC,
author = "Christine Choppy and Gianna Reggio",
title = "Improving Use Case Based Requirements Using Formally
Grounded Specifications (Complete Version)",
year = "2003",
institution = "Univ. of Genova",
type = tech-rep,
number = "DISI-TR-03-45",
URL = "ftp://ftp.disi.unige.it/person/ReggioG/ChoppyReggio03c.pdf",
url-ps = "ftp://ftp.disi.unige.it/person/ReggioG/ChoppyReggio03c.ps",
month = oct,
note = "A short version is to appear in Proc. FASE 2004",
abstract = "Our approach aims at helping to produce adequate
requirements, both clear and precise enough so as to
provide a sound basis to the overall development. Our
idea here is to find a way to combine both advantages
of use cases and of formal specifications. We present a
technique for improving use case based requirements,
using the formally grounded development of the
requirements specification, and that results both in an
improved requirements capture, and in a requirement
validation. The formally grounded requirements
specification is written in a ``visual'' notation,
using both diagrams and text, with a formal counterpart
(written in the Casl and Casl-Ltl languages). Being
formally grounded, our method is systematic, and it
yields further questions on the system that will be
reflected in the improved use case descriptions. The
resulting use case descriptions are of high quality,
more systematic, more precise, and its corresponding
formally grounded specification is available. We
illustrate our approach on part of the Auction System
case study.",
annote = "Presents a technique for improving use case based
requirements, using the formally grounded development
of the requirements specification (in \textsc{Casl} and
\textsc{Casl-Ltl}).",
}
@Book{CoFI:2004:CASL-RM,
author = "{CoFI (The Common Framework Initiative)}",
title = "\textsc{Casl} Reference Manual",
year = "2004",
publisher = pub-springer,
series = lncs # "2960 (IFIP Series)",
annote = "Gives full details of the design of \textsc{Casl}: an
informal language summary, concrete and abstract
syntax, well-formedness and model-class semantics, and
proof rules. Includes the libraries of basic
datatypes.",
note = {Free online version available at \url{http://www.cofi.info}},
}
@InCollection{CoFI:2004:CASL-Summary,
author = "{CoFI Language Design Group}",
title = "\textsc{Casl} Summary",
chapter = "I",
type = "Part",
note = "Edited by B.~Krieg-Br{\"u}ckner and P.~D.~Mosses",
crossref = "CASL-RM",
annote = "Gives an informal summary of the \textsc{Casl}
constructs for basic, structured, architectural, and
library specifications. Defines sublanguages and lists
proposed extensions of \textsc{Casl}.",
}
@InCollection{CoFI:2004:CASL-Syntax,
author = "{CoFI Language Design Group}",
title = "\textsc{Casl} Syntax",
chapter = "II",
type = "Part",
note = "Edited by B.~Krieg-Br{\"u}ckner and P.~D.Mosses",
crossref = "CASL-RM",
annote = "Defines the lexical, concrete, and abstract syntax of
\textsc{Casl}.",
}
@InProceedings{Coscia:1999:JJT,
author = "Eva Coscia and Gianna Reggio",
title = "{JTN}: {A} {Java}-Targeted Graphic Formal Notation for
Reactive and Concurrent Systems",
pages = "77--97",
crossref = "FASE-99",
annote =
"JTN is a formal graphic notation for Java-targeted
design specifications
(i.e., of systems that will be
implemented using Java).",
}
@Article{Costa:1997:SAD,
author = "Gerardo Costa and Gianna Reggio",
title = "Specification of Abstract Dynamic DataTypes: {A}
Temporal Logic Approach",
journal = tcs,
year = "1997",
volume = "173",
number = "2",
pages = "513--554",
annote = "Proposes a logic which combines
many-sorted first-order logic with branching-time
combinators for the
specification of dynamic-data types.",
}
@Article{Haveraaen:1999:FSE,
author = "Magne Haveraaen and Helmer Andr{\'e} Friis and Tor
Arne Johansen",
title = "Formal Software Engineering for Computational
Modeling",
journal = njc,
year = "1999",