@comment { File : $Source: /home/cvs/cvsroot/projects/visualstate/papers/pubs.bib,v $ Comment: Global bibtex file (anything on statecharts, code generation, programming languages etc. Only one criterium: I found it and perhaps read it while working on this project :). $Id: pubs.bib,v 1.180 2004/05/04 17:57:41 wasowski Exp $ } @comment { max paper used: 0055 FIXME: 51 is used already for something. Fix it (I have lost the file) max binder used: 007 } @comment{ BINDERS : 001 - Formal semantics of programming languages (nearly FULL) 002 - Software Engineering, Generative Programming, Partial Evaluation 003 - Semantics of Statecharts and similar 004 - slicing and TESTING 005 - code generation from statecharts (and similar) 006 - papers on verification (not the course itself) 007 - Argos, Lustre, Signal Synccharts, modecharts } @comment { PhD dissertations related to my work: Rohit Jain: o weryfikacji (to jest tylko Bsc!) Drusinski-Yoresh: Hung Ledang, mam wydrukowane, po francusku (ten gostek od B-method) Lind-Nielsen see below: lind-nielsen:2000 mam Erpenbach see below mam Claude Ackad mam, po niemiecku Kirill Bogdanov Testing statecharts, mam, see below M. Spreng Rapid prototping... (czy to jest doktorat czy magisterka?) H.P. Nguyen. Derivation De Specifiactions Formelles B a Partir De Specifications Semi Formelles. Doctoral thesis, Centre d'Etudes et de Recherche en Informatique du CNAM, 1998 Gerd Behrmann mam nawet wydrukowane Alexandre David Huppal Olivier Moeller mam, tam jest splaszczanie huppaal do uppaal } % ---- Latex Macros for processing this file % see companion p. 404 @comment{@preamble{ "\newcommand{\mycommanda}[1]{#1} " # "\newcommand{\mycommandb}[1]{#1} "}} % ---- Publishers and institutions @string{sv="Springer-Verlag"} @string{cup="Cambridge University Press"} @string{oup="Oxford University Press"} @string{mit="The {MIT} Press"} @string{jws="John Wiley \& Sons"} @string{aw="Addison-Wesley"} @string{esp="Elsevier Science Publishers"} @string{aca="Academic Press"} @string{mcgraw="McGraw--Hill"} @string{kaufmann="M. Kaufmann Publishers"} @string{vnr="Van Nostrand Reinhold"} @string{vnny="Van Nostrand, New York"} @string{bib="Bibliopolis"} @string{nh="North Holland"} @string{ph="Prentice Hall"} @string{plenum="Plenum"} @string{osp="Oxford Science Publishers"} @string{hup="Harvard University Press"} @string{aws="Almquist \& Wiksell, Stockholm"} @string{perg="Pergamon, Oxford"} @string{ahl="Ellis Horwood Limited"} @string{acm="ACM Press"} @string{ieee="IEEE Computer Society Press"} @string{claren="Clarendon Press"} @string{birk="Birkh{\"a}user"} @string{ora="O'Reilly and Associates"} @string{usenix="{USENIX} Association"} @string{itu="IT University of Copenhagen"} @string{kap="Kluwer Academic Publishers"} @string{irisa="Institut de Recherche en Informatique et Systemes Al\'eatoires ({IRISA})"} @comment{ --- series && journals } @string{acmcs="ACM Computing Surveys"} @string{fmsd="Formal Methods in System Design"} @string{isics="International Series in Computer Science"} @string{jacm="Journal of ACM"} @string{lncs="Lecture Notes in Computer Science"} @string{tose="{IEEE} Transactions on Software Engineering"} @string{tosem="{ACM} Transactions on Software Engineering and Methodology"} @string{tocad="{IEEE} Transactions on Computer-Aided Design"} @string{toplas="{ACM} Transactions on Programming Languages and Systems"} @string{ieeec="{IEEE} Computer"} @string{comm="Communications of the {ACM}"} @string{scp="Science of Computer Programming"} @string{ph-cs="Prentice Hall International Series in Computer Science"} @comment{ --- entries } % :AB @book{ abelson:1985, AUTHOR = {H. Abelson and G. Sussman}, TITLE = {Structure and Interpretation of Computer Programs}, PUBLISHER = {MIT Press, Cambridge, Mass.}, YEAR = {1985}, SUMMARY = {A classic book, now available online: http://mitpress.mit.edu/sicp} } % :AC @inproceedings{ ackad:1998, AUTHOR = {Claude Ackad}, TITLE = {Software Synthesis from Statechart Models for Real Time Systems}, BOOKTITLE = {International Workshop on Distributed and Parallel Embedded Systems (DIPES'98)}, YEAR = 1998, PUBLISHER = kap, ADDRESS = {Paderborn,Germany}, PAGES = {73--81}, EDITOR = {Rammig, F.J.}, SUMMARY = {Claude compiles statecharts to sequential code. Somewhat mysteriously seems to perform WCET analysis on chunks of C code doing this for specific platform (kind of high level to do this kind of things - he is not referring to any tools). He compiles via PEG (execution graphs) which seem to be a crucial point of the approach - he refreins to define and describe those graphs in details - sad. Transitions are ordered in a way which somehow decreases the number of double-buffering needed.}, AWNOTE = {code-generation binder} } @comment{ :AL } @InProceedings{ alfaro/henzinger:2001a, author = {Luca de Alfaro and Thomas A. Henzinger}, title = {Interface Automata}, booktitle = {Proceedings of the Ninth Annual Symposium on Foundations of Software Engineering (FSE)}, pages = {109--120}, year = 2001, address = {Vienna, Austria}, month = sep, publisher = acm } @book{ alhir:1998, AUTHOR = {Sinan Si Alhir}, TITLE = {UML in a Nutshell}, PUBLISHER = {O'Reilly \& Associates, Inc.}, ADDRESS = {101 Moris Street, Sebastopol, CA 95472}, YEAR = {1998}, SUMMARY = {UML description aimed at end-users. Just a book of4 quality many have: you will find several in each mainstream computer bookshops. I warn you before readin it: you take the risk yourself. It is extremely boring indeed. Otherwise it contains a description of state diagrams in chapter eleven which is the most rigorous comparing to what I have seen in other similar books. Still probably the definition of UML is the primary resource giving more on that.} } @inproceedings{ali/tanaka:1999, AUTHOR = {Jauhar Ali and Jiro Tanaka}, TITLE = {Converting Statecharts into {Java} Code}, BOOKTITLE = {5th International Conference on Integrated Design and Process Technology (IDPT'99)}, YEAR = 1999, MONTH = jun, ADDRESS = {Dallas,Texas}, SUMMARY = {This is a generalization of state pattern mentioned by Zuendorf. The extension is by introducing AND states. This is no longer so nice (cannot be encoded in OO type system) so more actual delagations have to be generated, which makes the impression that this should work slowly. Gives the reference to actual "state pattern".} } @techreport{ alstrup/rauhe:2001a, AUTHOR = {Stephen Alstrup and Theis Rauhe}, TITLE = {Improved Labeling Schemes for Ancestor Queries}, YEAR = 2001, MONTH = aug, INSTITUTION = itu, ADDRESS = {Denmark}, NUMBER = {TR 2001-5}, SUMMARY = {An introduction contains a brief survey of labelling schemes.}, AWNO = 0008, AWBI = 005 } @inproceedings{ alur/etal:1999a, AUTHOR = {Rajeev Alur and Sampath Kannan and Mihalis Yannakakis}, TITLE = {Communicating Hierarchical State Machines}, BOOKTITLE = {26th International Colloquium on Automata, Languages and Programming (ICALP)}, YEAR = 1999, MONTH = jul, PUBLISHER = sv, SERIES = lncs, VOLUME = 1644, ADDRESS = {Prague, Czech Republic}, PAGES = {169--178}, EDITOR = {Jir\'{\i} Wiedermann and Peter van Emde Boas and Mogens Nielsen}, URL = {http://www.springerlink.com/link.asp?id=980rt2de1mqqu2ll}, AWBI = 006, AWNO = 0040, SUMMARY = {Discussion on what is the impact of introducing hierarchy on complexity of decision problems for state machines and the succintness of representation. Unfortunately lots of details are left out and there have not been any Journal version until now, which would be very useful.} } @article{alur/yannakakis:2001, AUTHOR = {Rajeev Alur and Mihalis Yannakakis}, TITLE = {Model checking of hierarchical state machines}, JOURNAL = toplas, VOLUME = 23, NUMBER = 3, YEAR = 2001, MONTH = may, ISSN = {0164-0925}, PAGES = {273--303}, URL = {http://doi.acm.org/10.1145/503502.503503}, PUBLISHER = acm, SUMMARY = {The aim is to give algorithms and theoretical bounds on complexity of model checking problems for hierarchical state machines. This is on purpose studied in sepration from concurrency. They consider three problems, two in automata teorethic setting and one in symbolic model checking setting. Apparently addition of hierarchy decreases size of the model exponentially, but the cost of model-checking does not increase exponentially.}, AWNO = 0023, AWBI = 006 } @inproceedings{ amagbegnon/etal:1995, AUTHOR = {Pascalin Amagb\'egnon and Lo\:ic Besnard and Paul Le Guernic}, TITLE = {Implementation of the data-flow synchronous language {SIGNAL}}, BOOKTITLE = {ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)}, YEAR = 1995, ISBN = {0-89791-697-2}, PAGES = {163--173}, LOCATION = {La Jolla, California, United States}, URL = {http://doi.acm.org/10.1145/207110.207134}, PUBLISHER = acm, SUMMARY = {Contains a short nice and clear description of Signal. The best I found probably. Then Signal is compiled to big nested if-then-else structure in rather optimal and interesting way. The problem is that the compiler tries to reconstruct some kind of hierarchy, probably arriving at hierarchy similar to the one in original statechart, which is lost in earlier phase of translation} } @inproceedings{amnell/etal:2001, AUTHOR = {Tobias Amnell and Elena Fersman and Paul Pettersson and Wang Yi}, TITLE = {Automatic Code Synthesis for Timed Automata}, BOOKTITLE = {NWPT'01 -- The 13th Nordic Workshop on Programming Theory}, YEAR = 2001, MONTH = oct, ADDRESS = {Lyngby, Denmark}, SUMMARY = {Very brief abstract on generating code from UPPAAL models. The code should be time safe (meet the time constraints). Its based on tasks and scheduling} } @inproceedings{andre/peraldi:1993, AUTHOR = {Charles Andr\'e and Marie-Agne\`es P\'eraldi}, TITLE = {Effective Implementation of {ESTEREL} Programs}, BOOKTITLE = {5th EUROMICRO Workshop on Real-Time Systems}, YEAR = {1993}, MONTH = jun, PUBLISHER = ieee, ADDRESS = {Oulu, Finland}, PAGES = {262--267}, SUMMARY = {Relatively simple proposition how to adapt Esterel (and other synchronous control languages with their own kernel core) to some of real time requirements. Rather simple and directly applicable to our - statecharts - case.} } @techreport{ andre:1995, AUTHOR = {Charles Andr\'e}, TITLE = {{SyncCharts}: A Visual Representation of Reactive Behaviors}, YEAR = 1995, MONTH = oct, INSTITUTION = {I3S, Sophia-Antipolis}, ADDRESS = {France}, NUMBER = {TR 95-52}, SUMMARY = {The very basic (fundamental) description of synccharts} } @inproceedings{ andre:1996a, AUTHOR = {Charles Andr\'e}, TITLE = {Representation and Analysis of Reactive Behaviors: A Synchronous Approach}, BOOKTITLE = {Proceedings of Computational Engineering of Systems Applications (CESA)}, MONTH = jul, YEAR = 1996, PUBLISHER = {IEEE-SMC}, PAGES = {19--29}, ADDRESS = {Lille, France}, SUMMARY = {Original version of andre:1996b} } @techreport{ andre:1996b, AUTHOR = {Charles Andr\'e}, TITLE = {Representation and Analysis of Reactive Behaviours: A Synchronous Approach}, YEAR = 1996, INSTITUTION = {Laboratoire Informatique, Signaux, Syst\`emes (I3S)}, ADDRESS = {Nice, France}, NUMBER = {TR 96-28}, SUMMARY = {Description of SyncCharts: variant of statecharts with preemption.} } @inproceedings{andre/etal:2001a, AUTHOR = {Charles Andr\'e and Fr\'ed\'eric Boulanger and Alain Girault}, TITLE = {Software Implementation of Synchronous Programs}, BOOKTITLE = {2nd International Conference on Application of Concurrency to System Design (ACSD)}, YEAR = 2001, MONTH = jun, PUBLISHER = ieee, ADDRESS = {Newcastle upon Tyne, UK}, PAGES = {133--142}, SUMMARY = {A description of technical solutions undertaken in implementation of synchronous applications, taking into account that the enviornment (not the machine) is inherently asynchronous. The paper does not rely too much on the strong synchrony hypothesis of Esterel. It could be written equaly well using another para-synchronous language (like statecharts). Thus it can be used as a gentle introducion of time matters to synchronous like progrmaming (state/event based programming)} } @article{ appel/jacobson:1988, AUTHOR = {Andrew W. Appel and Guy J. Jacobson}, TITLE = {The World's Fastest Scrabble Program}, JOURNAL = comm, YEAR = 1988, VOLUME = 31, NUMBER = 5, PAGES = {572-578.585}, SUMMARY = {Graph representation of tree (TRIE) storing a lexicon. Probably influenced people working on finite automata and dictionaries. Apparently not very useful for code generation} } %%% :BE @inproceedings{ beauvais/etal:1998a, AUTHOR = {J.-R. Beauvais and T. Gautier and Paul Le Guernic and R. Houdebine and E. Rutten}, TITLE = {A translation of Statecharts into Signal}, BOOKTITLE = {International Conference on Application of Concurrency to System Design (ACSD'98)}, YEAR = 1998, MONTH = mar, ADDRESS = {Aizu-Wakamatsu, Japan}, SUMMARY = {As stated in the title. Also gives a short introduction to Signal. Unfortunately omits details about the next step of translation DC -> C++. beavais/etal:1998 is an extended TR. There is also a journal version available. Of those three this one is the shortest.} } @techreport{ beauvais/etal:1998, AUTHOR = {J.-R. Beauvais and R. Houdebine and P. Le Guernic and E. Rutten and T. Gautier}, TITLE = {A translation of {Statecharts} and {Activitycharts} into {Signal} equations}, YEAR = 1998, MONTH = may, INSTITUTION = irisa, ADDRESS = {Rennes Cedex, France}, NUMBER = 1182, ISSN = {1166-8687} } @inproceedings{ beeck:1994, AUTHOR = {Michael von der Beeck}, TITLE = {A Comparison of Statecharts Variants}, BOOKTITLE = {ProCoS: Third International Symposium on Formal Techiniques in Real Time and Fault-Tolerant Systems.}, YEAR = 1994, PUBLISHER = sv, SERIES = lncs, VOLUME = {863}, PAGES = {128--148}, SUMMARY = {A readable survey once you know several statechart variants already. A quick catch-up on others. Increases understanding of general problems. May be a bit dry for a newcomer to the area.} } @article{ benveniste/etal:1991a, AUTHOR = {Albert Benveniste and Paul le Guernic and C. Jacquemot}, TITLE = {Programming with events and relations: the {Signal} language and its semantics}, JOURNAL = scp, YEAR = 1991, VOLUME = 16, PAGES = {103--149}, } @inproceedings{behrmann/etal:1999, AUTHOR = {G. Behrmann and K. G. Larsen and H. R. Andersen and H. Hulgaard and J. {Lind Nielsen}}, TITLE = {Verification of Hierarchical State/Event Systems using Reusability and Compositionality}, BOOKTITLE = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems ({TACAS})}, ADDRESS = {Amsterdam, The Netherlands}, PUBLISHER = sv, SERIES = lncs, VOLUME = 1579, PAGES = {163--177}, MONTH = mar, YEAR = 1999, SUMMARY = {Compositional backwards reachability technique extended for hierarchical models, without flattening, so it actually remains compositional. Flattening is criticized for high cost incurred in verification.}, AWNO = 0015, AWBI = 006 } @inproceedings{ behrmann/etal:1999a, AUTHOR = {Gerd Behrmann and Kaare Kristoffersen and Kim G.Larsen}, TITLE = {Code Generation for Hierarchical Systems}, BOOKTITLE = {NWPT'99 -- The 11th Nordic Workshop on Programming Theory}, ADDRESS = {Uppsala, Sweden}, YEAR = 1999, MONTH = sep, INSTITUTION = {Aalborg University}, SUMMARY = {Presents an idea of code generation scheme for hierarchical models. The current configuration is compressed to be n-tuple where n is ocmputed with a simple counter algorithm looking for the widest statically computable set of concurrent states. The optimization is the fact that for each guard its value is memoized. Memoization is invalidated whenever a transition invalidating the guard value is fired (this is precomputed). } } @article {behrmann/etal:2002a, AUTHOR = {G. Behrmann and K. G. Larsen and H. R. Andersen and H. Hulgaard and J. {Lind Nielsen}}, TITLE = {Verification of Hierarchical State/Event Systems using Reusability and Compositionality}, JOURNAL = fmsd, YEAR = 2002, VOLUME = 21, NUMBER = 2, PAGES = {225--244}, AWBI = 006, AWNO = 0048, SUMMARY = {A journal version of behrmann/etal:1999. Hierarchical CBR.} } @book{ berard/etal:2001, AUTHOR = {B. B\'erard and M. Bidoit and A. Finkel and F. Laroussinie and A. Petit and L. Petrucci and Ph. Schnoebelen and P. McKenzie}, TITLE = {Systems and Software Verification. Model-Checking Techniques and Tools}, PUBLISHER = sv, ADDRESS = {Berlin-Heidelberg}, YEAR = {2001}, URL = {http://www.springer.de/cgi-bin/search\_book.pl?isbn=3-540-41523-8}, SUMMARY = {Short student-oriented text book on verification. Contains a very brief chapter on BDDs which I read among other things on the topic. BDDs prove to be useful in analysis of statecharts at compile time. It seems that original Bryant's papers were more informative. Henrik Reif's note on BDDs is also much more detailed (and still very student-oriented). Otherwise a nice book for any newbie to verification. Also considers time. Last part enumerates and describes available model checkers (URL above is to Springer internet bookstore. Sorry ... no downloads). } } @incollection{ berry:2000a, AUTHOR = {G\'erard Berry}, EDITOR = {Gordon Plotkin and Colin Stirling and Mads Tofte}, BOOKTITLE = {Proof, Language and Interaction. Essays in Honour of Robin Milner}, TITLE = {The Foundations of {Esterel}}, PAGES = {425--454}, PUBLISHER = mit, YEAR = 2000, SERIES = {Foundations of Computing Series}, ADDRESS = {Cambridge, Massachusetts}, SUMMARY = {relatively short introduction to all aspects of esterel: reactivity, synchrone, syntax, semantics, compilation and verification. From my point of view it contains a brief explanation of to major code generation schemes: automaton based and circuit equations based.} } @misc{ berry:2000, AUTHOR = {G\'erard Berry}, TITLE = {The {Esterel} v5 Language Primer. Version~v5\_91}, YEAR = 2000, MONTH = jul, INSTITUTION = {Centre de Mathematiques Appliqu\'ees, Ecole des Mines and INRIA}, ADDRESS = {2004 Route des Lucioles, 06565 Sophia-Antipolis}, URL = {http://www-sop.inria.fr/meije/personnel/Gerard.Berry.html}, SUMMARY = {Simple Esterel programming textbook. Available at Esterel's website.} } @inproceedings{ caspi/etal:1987, AUTHOR = {P. Caspi and D. Pilaud and N. Halbwachs and J. Plaice}, TITLE = {Lustre: a declarative language for programming synchronous systems}, BOOKTITLE = {14th ACM Conference on Principles of Programming Languages (POPL)}, YEAR = 1987, MONTH = jan, PUBLISHER = acm, ADDRESS = {Munich}, SUMMARY = {Niestety tego jeszcze nie przeczytalem...} } @inproceedings{ chiodo/etal:1995, AUTHOR = {Massimiliano Chiodo and Paolo Giusto and Attila Jurecska and Luciano Lavagno and Harry Hsieh and Kei Suzuki and Alberto Sangiovanni-Vincentelli and Ellen Sentovich}, TITLE = {Synthesis of Software Programs for Embedded Control Applications}, BOOKTITLE = {32nd ACM/IEEE Design Automation Conference}, YEAR = 1995 } @comment{ :CL } @Book{ clarke:1999a, author = {Edmund M. Clarke}, title = {Model Checking}, publisher = mit, year = 1999, month = dec } @techreport{ clarke/heinle:2000, AUTHOR = {Edmund M. Clarke and Wolfgang Heinle}, TITLE = {Modular Translation of Statecharts to {SMV}}, YEAR = 2000, MONTH = apr, INSTITUTION = {School of Computer Science, Carnegie Mellon University}, NUMBER = {CMU-CS-00-XXX}, AWBI = 006, AWNO = 0017 } @comment{ :CO } @Book{ cormen/etal:2001a, author = {Thomas H. Cormen and Charles E. Leiserson and Ronald L. Rivest and Clifford Stein}, title = {Introduction to Algorithms}, publisher = mit, year = 2001, edition = {2nd} } @comment{ :BI } @book{ binder:2000a, AUTHOR = {Robert V. Binder}, TITLE = {Testing Object-Oriented Systems. Models, Patterns and Tools}, PUBLISHER = aw, YEAR = 2000, SUMMARY = {Part II, Chapter 7 on testing state machines contains a description of flattening statecharts of object oriented-hierarchy and then flattening and expansion of statechart hierarchy to a product machine. This machine may then be tested using flat methods. This is much further than one could expect from flattening for code generation, but still an interesting motivation for flattening.}, AWNOTE = {jcg has got a hardcopy. numbers refer to a photo copy of summarized pages}, AWNO = 0033, AWBI = 004 } % :BJ @inproceedings{bjorklund/etal:2001, AUTHOR = {Dag Bj{\"o}rklund and Johan Lilius and Ivan Porres}, TITLE = {Towards Efficient Code Synthesis from Statecharts}, BOOKTITLE = {Practical UML-Based Rigorous Development Methods - Countering or Integrating the eXtremists. Workshop of the pUML-Group.}, YEAR = 2001, MONTH = oct, PUBLISHER = {GI}, SERIES = {Lecture Notes in Informatics P-7}, ADDRESS = {Toronto,Canada}, EDITOR = {Andy Evans and Robert France and Ana Moreira Bernhard Rumpe}, SUMMARY = {A translation to intermediate SMDL language, which is then compiled using software graphs as in POLIS(?). The trans;lation starts with flattening (yuck), but then minimizes the S-graph. The paper is somewhat immature, especially the definition of SMDL part.} } % :BO @phdthesis{ bogdanov:2000a, AUTHOR = {Kirill Bogdanov}, TITLE = {Automated testing of Harel's statecharts}, SCHOOL = {The University of Sheffield}, YEAR = 2000, MONTH = jan, SUMMARY = {TODO}, AWBI = 004, AWNO = 0035, AWNOTE = {printed a chapter on flattening} } @article{ bogdanov/holcombe:2001a, AUTHOR = {Kirill Bogdanov and Mike Holcombe}, TITLE = {Statechart testing method for aircraft control systems}, JOURNAL = {Software Testing, Verification and Reliability}, YEAR = 2001, VOLUME = 1, NUMBER = 11, PAGES = {39--54}, SUMMARY = {Describes a testing method for hierarchical statecharts with no hierarchy and no history. As far as translation of statechart is concerned, this paper presents a flattening algorithm, which is also used in synthesis a lot. This particular flattening algorithm does cause exponential blow up, as the target language are statecharts. For each transition leaving from a superstate all possible source configurations are computed. However static conflict resolution is supported properly, by guard refinment (hard to said how smart it is though).}, AWBI = 004, AWNO = 0034 } @inproceedings{ bogdanov/holcombe:2002a, AUTHOR = {Kirill Bogdanov and Mike Holcombe}, TITLE = {Properties of concurrently taken transitions of {H}arel statecharts}, BOOKTITLE = {Workshop on Semantic Foundations of Engineering Design Languages (SFEDL)}, YEAR = 2002, MONTH = apr, ADDRESS = {Grenoble, France}, AWBI = 004, AWNO = 0036, SUMMARY = {This paper discusses the semantics of firing transitions, especially semantics of conflicts. It defines a new semantics of conflicts which coincides with that of pnueli/shalev:1991. This semantics has been widely use to statically resolve conflicts in flattening algorithms} } @article{bolyonkov:1984a, AUTHOR = {Mikhail A. Bulyonkov}, TITLE = {{Polyvariant Mixed Computation for Analyzer Programs}}, JOURNAL = {Acta Informatica}, VOLUME = 21, NUMBER = 5, PAGES = {473--484}, MONTH = dec, YEAR = {1984}, ISSN = {0001-5903 (print), 1432-0525 (electronic)}, ANNOTE = {An algorithm for mixed computation of low-level non-structured imperative programs is presented. The algorithm is shown to terminate and produce correct results when applied to the class of so-called analyzer programs, a definition of which is also given.} } @inproceedings{ bond/etal:2001, AUTHOR = {Gregory W. Bond and Franjo Ivancic and Nils Klarlund and Richard Trefler}, TITLE = {ECLIPSE Feature Logic Analysis}, BOOKTITLE = {2nd IP-Telephony Workshop}, YEAR = 2001, MONTH = apr, ADDRESS = {New York City, USA}, PAGES = {100--107}, SUMMARY = {Application of model-checker MOCHA to telecommunication protocols specified by statecharts. Statecharts are flattened before translating to MOCHA and a risk of exponential blow-up is mentioned.}, AWNO = {006/0019} } @book{booch/etal:1999, AUTHOR = {Grady Booch and James Rumbaugh and Ivar Jacobson}, TITLE = {The Unified Modelling Language: User Guide}, PUBLISHER = aw, YEAR = 1999, ISBN = {0-201-57168-4}, } @article{bryant:1986, AUTHOR = {Randal E. Bryant}, TITLE = {Graph-Based Algorithms for Boolean Function Manipulation}, URL = {http://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.ps}, JOURNAL = {{IEEE} Transactions on Computers}, VOLUME = 35, YEAR = 1986, PAGES = {677--691}, NUMBER = 8, MONTH = aug } @misc{ buddy, AUTHOR = {J{\o}rn {Lind Nielsen}}, TITLE = {{BuDDy} -- A Binary Decision Diagram Package Version 2.0}, NOTE = {http://www.it-c.dk/research/buddy}, URL = {http://www.it-c.dk/research/buddy}, SUMMARY = {BDD library implemented in C} } @inproceedings{ burch/etal:1990, AUTHOR = {{J.R. Burch} and {E.M. Clarke} and {K.L. McMillan} and {D.L. Dill} and {L.J. Hwang}}, TITLE = {{S}ymbolic {M}odel {C}hecking: $10^{20}$ {S}tates and {B}eyond}, BOOKTITLE = {Fifth Annual {IEEE} Symposium on Logic in Computer Science}, PUBLISHER = ieee, ADDRESS = {Washington, D.C.}, PAGES = {1--33}, YEAR = 1990 } %%% C: @book{czarnecki/eisenecker:2000, AUTHOR = {Krzysztof Czarnecki and Ulrich W. Eisenecker}, TITLE = {{Generative Programming: Methods, Tools, and Applications}}, PUBLISHER = aw, YEAR = 2000, SUMMARY = {This seems to be The Classic Book on generative programming. It is divided in 3 parts: domain engineering, implementation technology and examples. Despite the first part being the shortest it seems to be the one treated in most details. Implementation part (although rather fat) refers only superficially to multitude of technoleogies. Apparently the only thing really discussed in detail is C++ metaprogramming with templates (and various polymorphism issues). From my perspective this is an extremely restricted perspective. After reading this book you will only have the "hand-on" experience with one way of solving problems (object oriented programming, or even OOP in C++). The good word about the practical part is that it gives lots of clear explanations of fundamental programming and programming languages concepts, which are very useful for students.} } @inproceedings{czarnecki/etal:2002a, AUTHOR = {Krzysztof Czarnecki and Thomas Bednasch and Peter Unger and Ulrich Eisenecker}, TITLE = {Generative Programming for Embedded Software: An Industrial Experience Report}, BOOKTITLE = {Generative Programming and Component Engineering (GPCE)}, YEAR = 2002, MONTH = oct, PUBLISHER = sv, ADDRESS = {Pittsburgh, PA, USA}, SERIES = lncs, VOLUME = 2487, PAGES = {156--172}, EDITOR = {Don Batory and C. Consel and Walid Taha}, SUMMARY = {A suprisingly inconcrete example of application of GP to some satellite system. Uses template metaprogramming but this is not described in details. Instead authors focus on proposals to extension of feature modelling formalism.}, AWBI = 002, AWNO = 0004 } @comment :DA @article{ daciuk:2001, AUTHOR = {Jan Daciuk}, TITLE = {Experiments with Automata Compression}, JOURNAL = lncs, YEAR = 2001, VOLUME = 2088, PAGES = {105-112}, SUMMARY = {Nice representation methods, encodings, compressions aetrc for finite automata in language dictionary applications. This automata are acyclic but the methods used int the paper are not relying on that. We should be able to apply some to SM.Probably useful in last stage: generating a table representation.}, } @inproceedings{ damian/danvy:2001, AUTHOR = {Daniel Damian and Olivier Danvy}, TITLE = {Static Transition Compression}, BOOKTITLE = {Second International Workshop on Semantics, Applications, and Implementation of Program Generation (SAIG)}, SERIES = lncs, VOLUME = 2196, ADDRESS = {Florence, Italy}, YEAR = 2001, MONTH = sep, PAGES = {92--107}, PUBLISHER = sv, SUMMARY = {A nice short description of how to eliminate jump sequences in a C/Pascal like language} } @techreport{ david/moeller:2001, AUTHOR = {Alexandre David and M. Oliver M\"oller}, TITLE = {From {HUppaal} to {Uppaal}. {A} Translation from Hierarchical Timed Automata to Flat Timed Automata}, YEAR = 2001, MONTH = mar, INSTITUTION = {BRICS}, NUMBER = {RS-01-11}, ISSN = {0909-0878}, SUMMARY = {Yet another, earlier, version of flattening published in david/etal:2002}, AWBI = 006, AWNO = 0013 } @inproceedings{ david/etal:2002, AUTHOR = {Alexandre David and M. Oliver M\"oller and Wang Yi}, TITLE = {Formal Verification of {UML} Statecharts with Real-Time Extensions}, BOOKTITLE = {Fundamental Approaches to Software Engineering (FASE)}, YEAR = 2002, MONTH = apr, PUBLISHER = sv, SERIES = lncs, VOLUME = 2306, ADDRESS = {Grenoble, France}, PAGES = {218--232}, EDITOR = {Ralf-Detlef Kutsche and Herbert Weber}, SUMMARY = {A description of model-checker for statecharts with time, which will (were?) hopefully included in UML profile for real time. The main idea is to translate UML statecharts to flat timed automata and use Uppaal to verify the model. Paper formalises the syntax and semantics of statecharts, while it treats the crucial flattening process slightly superficially. Complexity is not mentioned but it can be understood from the description that timed automata description can be exponentially bigger than UML statechart source. See corresponding TR from Uppsala for more details.}, AWBI = 006, AWNO = 0011 } @techreport{ david/etal:2003, AUTHOR = {Alexandre David and M. Oliver M\"oller and Wang Yi}, TITLE = {Verification of {UML} Statechart with Real-time Extensions}, YEAR = 2003, MONTH = feb, INSTITUTION = {Department of Information Technology, Uppsala University}, NUMBER = {2003-19}, ISSN = {1404-3203}, SUMMARY = {Extended version of david/etal:2002. This one is detailed indeed. It also goes into all kinds of technicalities of flattening.}, AWBI = 006, AWNO = 0012 } @comment{ -- :DE: } @article{ demicheli/etal:1985, AUTHOR = {Giovanni de Micheli and Robert K. Brayton and Alberto Sangiovanni-Vincentelli}, TITLE = {Optimal State Assignment for Finite State Machines}, JOURNAL = tocad, YEAR = 1985, VOLUME = {CAD-4}, NUMBER = 3, PAGES = {269--285}, SUMMARY = {Nice basic definitions for the problem of state assignment. They only consider a simple FSM. No hierarchy. No concurrency. I do not understand all the hardware details, but those seem irrelevant to the core of the work.} } @comment{ -- :DI } @incollection{ diekert/metivier:1997, AUTHOR = {Volker Diekert and Yves M\'etivier}, TITLE = {Partial Commutation and Traces}, PAGES = {457--533}, CROSSREF = {rozenberg/salomaa:1997}, SUMMARY = {This theory is useful for describing somewhat nondeterministic semantics of statecharts, namely nondeterminism arising bcs of independent processing of transitions and independent processing of children in and-states.}, AWNOTE = {The numbers refer to a draft copy published as a technical report}, AWBI = 003, AWNO = 0044 } @inproceedings{diethers/etal:2002a, AUTHOR = {Karsten Diethers and Ursula Goltz and Michaela Huhn}, TITLE = {Model Checking {UML} Statecharts with Time}, PAGES = {35--51}, CROSSREF = {CSDUML:2002}, AWNOTE = {in CSDUML proceedings booklet}, SUMMARY = {They translate statecharts into UPPAAL TAs, much like the above papers by david/etal:2002. They claim this is different because they treat events fully (apparently the two things were developed sort of in parallel, unaware of each other). They assumed that time elapses only if event queue is empty (synchrony hypothesis, isn't it?). I dare to claim that this is not very useful, bcs this way the time took by action execution seems to be ignored. Only XOR states are allowed, no concurrency in the statechart... but at least they allow to compose a bunch of statecharts together (this is my impression). No history, unclear about entry/exits. The translation is two stage -- flattening is used explicitly first and then the flat statechart is translated to TA.} } @comment{ --- :DR } @phdthesis{ drusinsky:1988a, AUTHOR = {Doron Drusinsky}, TITLE = {On Synchronized Statecharts}, SCHOOL = {Department of Applied Mathematics, Weizmann Institute of Science, Rehovot, Israel}, YEAR = {1988} } @inproceedings{ drusinsky/harel:1988, AUTHOR = {Doron Drusinsky and David Harel}, TITLE = {On the Power of Cooperative Concurrency}, BOOKTITLE = {Proceedings of Concurrency '88}, YEAR = 1985, PUBLISHER = sv, SERIES = lncs, VOLUME = 335, ADDRESS = {New York}, PAGES = {74--103}, } @article{ drusinsky/harel:1994a, AUTHOR = {Doron Drusinsky and David Harel}, TITLE = {On the Power of Bounded Concurrency {I}: Finite Automata}, JOURNAL = jacm, VOLUME = 41, NUMBER = 3, YEAR = 1994, MONTH = may, PAGES = {517--539}, URL = {http://doi.acm.org/10.1145/176584.176587}, AWBI = 005, AWNO = 0039, SUMMARY = {A Journal version of drusinsky/harel:1988. It discusses results about succintness of various concurrency formalism (NDA, DFA, AFA and alternating statecharts, deterministic statecharts and A-statecharts (universal statecharts)). The results are interesting (indicate exponential, additive differences in succintness between various pairs). ACM DL has a nice, detailed review published, also the articles abstract makes a good summary of results. This paper is far more comprehensible (and contains more results) than the previous conference version. Contrary to common opinions this paper does *not* show that hierarchical statecharts with concurrency as exponentially more succint than flat statecharts. This result can be attirbuted to alur/etal:1999a, though not entirely} } @article{ drusinsky/harel:1989, AUTHOR = {Doron Drusinsky and David Harel}, TITLE = {Using Statecharts for Hardware Description and Synthesis}, JOURNAL = tocad, YEAR = 1989, VOLUME = 8, NUMBER = 7, PAGES = {798--807}, SUMMARY = {Describes how to flatten the statecharts to nearly a set of Mealy machines without exponential blow up. It seems to be very similar to what I have invented some time ago, roughly 15 years later than authors, who BTW manged to get a patent protection on that. Contains the classic traffic lights controller example model. Half of the paper contains informl description of statecharts and this model. Then there is a small section on this flattening (section IV in the begining) and than there is lots of hardware staff irrelevant for us.} } @article{drusinsky-yoresh:1990, AUTHOR = {Doron Drusinsky-Yoresh}, TITLE = {Symbolic Cover Minimization of Fully {I/O} Specified Finite State Machines}, JOURNAL = tocad, YEAR = 1990, VOLUME = 9, NUMBER = 7, PAGES = {779--781}, SUMMARY = {A version of famous Nerod's theorem about automata minimization for hierarchical state machines (HFSM), namely statecharts without concurrency. The HFSM must be fully specified symbolically as a complete set of rules. Also note that this is a full minimization theorem for sequential statecharts, or better sequential statecharts without guards (?). The minimization problem for statecharts with concurrency is probably intractable.} } @article{ drusinsky-yoresh:1991a, AUTHOR = {Doron Drusinsky-Yoresh}, TITLE = {A State Assignment Procedure for Single-Block Implementation of State Charts}, JOURNAL = tocad, YEAR = 1991, VOLUME = 10, NUMBER = 12, PAGES = {1569--1576}, SUMMARY = {Good description of appraoch to minimize the length of global state vector (GSV). Not optimal though. Patented. The article is hardware oriented but it seems the method is well adaptable to software.} } @article{ drusinsky-yoresh:1991b, AUTHOR = {Doron Drusinsky-Yoresh}, TITLE = {Decision Problems for Interacting Finite State Machines}, JOURNAL = tocad, YEAR = 1991, VOLUME = 10, NUMBER = 12, PAGES = {1576--1579}, SUMMARY = {Proves following properties to be PSPACE for communicating FSMs: veryfing systems determinism, testing the existence of unspecified inputs, testing gor exclusiveness of two internal FSM signals.} } @comment :EN @InProceedings{engels/etal:2001a, author = {Gregor Engels and Reiko Heckel and Jochen Malte K\"uster}, title = {Rule-Based Specification of Behavioral Consistency Based on the {UML} Meta-model}, crossref = {UML:2001}, pages = {272--286}, awno = 0052, awbi = 002, summary = {This paper considers behavioral consistency between various UML diagrams. In practice the appraoch is demonstrated on class inheritance, with statecharts defining usage protocol of classes. The notion of consistency is expressed using trace refinment of CSP. The paper contains a CSP semantics for a subset of statecharts (non-concurrent). They use the FDR tool to verify trace refinement. The paper contains a tiny UML metamodel. Just a small subset of statecharts and class diagrams.} } @comment :ER @inproceedings{ erpenbach/altenbernd:1999, AUTHOR = {Edwin Erpenbach and Peter Altenbernd}, TITLE = {Worst-Case Execution Times and Schedulability Analysis of Statecharts Models}, BOOKTITLE = {11th Euromicro Conference on Real Time Systems}, YEAR = 1999, ADDRESS = {York}, SUMMARY = {Very similar to other papers by E. Erpenbach in 1999. Actually only differs in analysis of last sections. The rest seems to be a basic cut and paste.} } @inproceedings{ erpenbach/etal:1999a, AUTHOR = {Edwin Erpenbach and Friedhelm Stappert Joachim Stroop}, TITLE = {Compilation and Timing Analysis of Statecharts Models for Embedded Systems}, BOOKTITLE = {In The Second International Workshop on Compiler and Architecture Support for Embedded Systems (CASES)}, YEAR = 1999, MONTH = oct, ADDRESS = {Washington, D.C, USA}, SUMMARY = {Rather non informative paper. Describes a code generator for statecharts (embedded systems are the purpose), but actually does not even give a hint of how the code is generated. The model language seems to accept pure signals (in esterel spirit). Models are execcuted asynchronously: 1 process collecting incoming events and one producing reactions (the statechart engine). They do some schedulability analysis, but it is unclear how. I guess how is described in other 1999 paper, but I am not sre if the approach is sound. Anyway the first ever c;ear description how one would execute statecharts in time aware way.} } @inproceedings{ erpenbach/etal:1999, AUTHOR = {Edwin Erpenbach and Joachim Stroop and Franz J. Rammig}, TITLE = {On the compilation of Statecharts Models into Target Code}, BOOKTITLE = {{IEEE} International Symposium on Computer Aided Control System Design Kohala Coast-Island of Hawai'i, USA}, YEAR = 1999, PUBLISHER = ieee, PAGES = {249--254}, SUMMARY = {Finally a paper which is close to what I do. Shows how verification like approach may help us to perform optimizations. They compute the worst case number of iteration steps for STATEMATE model and use it to optimize the code generation. Fixed number of iterations is used instead of flagged assignments. This specific optimization is not useful for VisualSTATE because VS models are not so much synchonous. Still the whole approach opens a bunch of possibilities for us} } @article{ ernst/etal:1997, AUTHOR = {Jens Erns and Wiliam Evans and Christopher W. Fraser and Steven Lucco and Todd A. Proebsting}, TITLE = {Code compression}, JOURNAL = {Proceedings of the ACM SIGPLAN'97}, YEAR = 1997, VOLUME = 6, PAGES = {358--365}, SUMMARY = {Two approaches: double stream compression and before-execution-decompression and second: combining and specializing instructions with dictionary method.} } @phdthesis{ erpenbach:2000, AUTHOR = {Edwin Erpenbach}, TITLE = {Compilation, Worst-Case Execution Times and Schedulability Analysis of Statecharts Models}, SCHOOL = {Department of Mathematics and Computer Science of the University of Paderborn}, MONTH = apr, YEAR = 2000, SUMMARY = {Edwin's dissertation. Has much more focus on the entire infrustructure that SCOPE has not got currently. Considers interaction with RTOS, timing analysis, etc, while I mostly consider size and speed of the implementation itself and leave the rest aside (which is of course important, but somewhat orthogonal). The control code itself is hierarchical, based on nested switch statements (targetting C). Considers several optimizations, one of them seems to be advanced (minimizing double bufferring). Remaining are rather minor (not counting WCNIS analysis which is advanced and complex, but I am not sure if it really brings an improvemnt - may be it brings in size. Nevertheless in current VS version of language we compile there is need for WCNIS analysis at all, due to lack of "self-firing" transitions). Also luckily the optimizations he considers are different from those I am planning. Also contains complete source code for tailligth controller (Rhapsody in MicroC example program). A drawback of the dissertations is an extremly small number of experimental results and lack of information on how given results were measured (platforms, C-compiler, optimizations in mind, etc). } } @comment :ES @inproceedings{ eshuis/wieringa:2000, AUTHOR = {Rik Eshuis and Roel Wieringa}, TITLE = {Requirements Level Semantics for {UML} Statecharts}, BOOKTITLE = {Formal Methods for Open Object-Based Distributed Systems IV - Proc. FMOODS'2000, September, 2000, Stanford, California, USA}, YEAR = 2000, EDITOR = {Scott F. Smith and Carolyn L. Talcott}, PUBLISHER = kap, SUMMARY = {no history treatment, no elements (variables), some restrictions on UML similar to visual STATE. Quite a good insight to different properites of statechart.} } @comment :ET @Article{etalle/gabbrieli:1998a, author = {Sandro Etalle and Maurizo Gabbrieli}, title = {Partial evaluation of concurrent constraint languages}, journal = acmcs, publisher = acm, year = 1998, doi = {http://doi.acm.org/10.1145/289121.289132}, volume = 30, number = {3es}, month = sep, summary = {A short survey explaining why partial evaluation (PE) should be more successful for concurrent constraint languages than for typical concurrent languages (CCS/CSP-like). Contains some references to PE of concurrent languages}, annote = {special issue: electronic supplement to the September 1998 issue}, awbi = 002, awno = 0055 } @comment :FI @book{ fischer/leblanc:1991, AUTHOR = {Charles Fischer and Richard LeBlanc}, TITLE = {Crafting a Compiler}, SUMMARY = {should contain a chapter on local code optimization}, PUBLISHER = aw, YEAR = {New revised edition is coming soon (early 2002).}, EDITION = {2nd} } @article{ flinn/etal:2001, AUTHOR = {Jason Flinn and Eyal de Lara and Mahadev Satyanarayanan and Dan S. Wallach and Willy Zwaenepoel}, TITLE = {Reducing the Energy Usage of Office Applications}, JOURNAL = lncs, YEAR = 2001, VOLUME = 2218, PAGES = {252--272}, KEYWORD = {power saving}, SUMMARY = {Description of distilling interface between PowerPoint and its document file which reduces the energy usage upto 50\%. Not particularly useful in terms of Embedded Systems} } @article{fraser/wendt:1986, AUTHOR = {Christopher W.Fraser and Alan L. Wendt}, TITLE = {Integrating Code Generation and Optimization}, JOURNAL = {SIGPLAN Notices}, YEAR = 1986, MONTH = jun, VOLUME = 21, NUMBER = 7, PAGES = {242--248}, } @comment{ --- :GA } @article{ ganapathi/etal:1982, AUTHOR = {M. Ganapathi, C.N. Fisher, J.L. Henessy}, TITLE = {Retargetable Compiler Code Generation}, JOURNAL = {ACM Computing Surveys}, YEAR = 1982, VOLUME = 14, NUMBER = 4 } @inproceedings{ gray:1988, AUTHOR = {R. Gray}, TITLE = {A generator for lexical analyzers that programmers can use}, BOOKTITLE = {USENIX Conference}, PAGES = {147--160}, YEAR = 1988, MONTH = jun } @comment{ --- :HA } @article{ halbwachs/etal:1991, AUTHOR = {Nicholas Halbwachs and Paul Caspi and Pascal Raymond and Daniel Pilaud}, TITLE = {The Synchronous Data Flow Programming Language {LUSTRE}}, JOURNAL = {Proceedings of IEEE}, YEAR = 1999, MONTH = sep, VOLUME = 79, NUMBER = 9, PAGES = {1305--1320}, SUMMARY = {This papers defines syntax and semantics of Lustre (rather complete). The semantics is described much in informal way but one can easily see that underlying formalism can easily be developed. The paper is rather well written and gives a good introduction to Lustre for a beginner, including some properties of compiler and validation techniques. Compilation techniques are of certain interest for code generation for any reactive language (inluding statecharts).} } @incollection{ harel/pnueli:1985, AUTHOR = {David Harel and Amir Pnueli}, EDITOR = {Krzysztof R. Apt}, TITLE = {On the development of reactive systems}, BOOKTITLE = {Logic and Model of Concurrent Systems}, SERIES = {NATO ASI}, VOLUME = 13, PAGES = {477--498}, PUBLISHER = sv, MONTH = oct, YEAR = 1985, } @article{ harel:1987, AUTHOR = {David Harel}, TITLE = {Statecharts: A Visual Formalism for Complex Systems}, JOURNAL = {Science of Computer Programming}, YEAR = 1987, VOLUME = 8, PAGES = {231--274}, AWBINDER = 005, AWNO = 0046, SUMMARY = {Original definition of statecharts which was adopted later on for use in UML etc. Informal but quite descriptive. Contains an extensive wristwatch example which is probably considered classic.Would be nice to have it translated to visualSTATE} } @inproceedings{ harel/etal:1987, AUTHOR = {David Harel and Amir Pnueli and J.P.Schmidt and R.Sherman}, TITLE = {On the Formal Semantics of Statecharts}, BOOKTITLE = {2nd IEEE Symposium on Logic in Computer Science}, YEAR = 1988, PUBLISHER = ieee, ADDRESS = {New York}, PAGES = {396--406}, } @article{ harel/naamad:1996, AUTHOR = {David Harel and Amnon Naamad}, TITLE = {The {STATEMATE} Semantics of Statecharts}, JOURNAL = tosem, YEAR = 1996, VOLUME = 5, NUMBER = 4, PAGES = {293--333}, AWBI = 003, AWNO = 0041 } @article{harel/gery:1997, AUTHOR = {David Harel and Eran Gery}, TITLE = {Executable object modeling with statecharts}, JOURNAL = ieeec, PUBLISHER = ieee, YEAR = 1997, VOLUME = 30, NUMBER = 7, PAGES = {31--42}, ISSN = {00189162}, ABSTRACT = {Statecharts, popular for modeling system behavior in the structural analysis paradigm, are part of a fully executable language set for modeling object-oriented systems. The languages form the core of the emerging Unified Modeling Language. The authors embarked on an effort to develop an integrated set of diagrammatic languages for object modeling, built around statecharts, and to construct a supporting tool that produces a fully executable model and allows automatic code synthesis. The language set includes two constructive modeling languages (languages containing the information needed to execute the model or translate it into executable code).}, SUMMARY = {Brief, example based description of STATEMATE languages.} } @inproceedings{harel:1997a, AUTHOR = {David Harel}, TITLE = {Some Thoughts on Statecharts, 13 Years Later}, BOOKTITLE = {9th International Conference on Computer Aided Verification (CAV)}, YEAR = 1997, PUBLISHER = sv, SERIES = lncs, VOLUME = 1254, PAGES = {226--231}, EDITOR = {O. Grumberg}, } @techreport{harel/rumpe:2000, AUTHOR = {David Harel and Bernhard Rumpe}, TITLE = {Modeling Languages: Syntax, Semantics and All That Stuff}, YEAR = 2000, INSTITUTION = {The Weizmann Institute of Science}, ADDRESS = {Rehovot, Israel, MCS00-16}, URL = {http://www4.informatik.tu-muenchen.de/papers/HR00.html}, ABSTRACT = {The motivation for this paper, the first in a planned series of three parts, is the multitude of concepts surrounding the proper definition of complex modeling languages for systems and software, and the confusion that this often causes. Particularly relevant is the case of the recently standardized UML, which we refer to quite extensively as we proceed. Our intention is to discuss and clarify the notions involved in defining modeling languages. The main theme is the distinction between syntax and semantics, the nature and purpose of each, their usage and style, and the various means for defining and dealing with them. Underlying the exposition are the dichotomies of textual vs. visual languages, structural vs.~behavioral specification, and requirements vs. system models. We hope that the paper will be useful to language designers, methodologists, tool vendors and educators.}, AWBI = 001, AWNO = 0001 } @article{ harel/kupferman:2002, AUTHOR = {David Harel and Orna Kupferman}, TITLE = {On Object Systems and Behavioral Inheritance}, JOURNAL = tose, YEAR = 2002, MONTH = sep, VOLUME = 28, NUMBER = 9, PAGES = {889--903}, AWBI = 003, AWNO = 0005, SUMMARY = {Introduces the notion of behavioral inheritance for objects defined by state machines (not statecharts). Also discusses complexity issues which do not sound that promising}, } @book{hatcliff/etal:1999a, editor = {John Hatcliff and Torben \AE. Mogensen and Peter Thiemann}, title = {Partial Evaluation: Practice and Theory. DIKU 1998 International Summer School}, publisher = sv, year = 1999, volume = 1706, series = lncs, address = {Copenhagen, Denmark} } @inproceedings{henzinger/etal:2001a, AUTHOR = {Thomas A. Henzinger and Benjamin Horowitz and Christoph Meyer Kirsch}, TITLE = {Giotto: A Time-Triggered Language for Embedded Programming}, CROSSREF = {EMSOFT:2001}, PAGES = {166--184}, SUMMARY = {Seems to be the main paper introducing Giotto} } @inproceedings{henzinger/kirsch:2002a, AUTHOR = {Thomas A. Henzinger and Christoph M. Kirsch}, TITLE = {The Embedded Machine: Predictable, Portable Real-Time Code}, BOOKTITLE = {ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)}, YEAR = 2002, ADDRESS = {Berlin,Germany}, PAGES = {315--326}, SUMMARY = {The main paper introducing E machine} } @book{hoare:1985a, AUTHOR = {C.A.R. Hoare}, TITLE = {Communicating Sequential Processes}, PUBLISHER = ph, SERIES = isics, YEAR = 1985 } @book{ hopcroft/ullman:1979, AUTHOR = {John E. Hopcroft and Jeffrey D. Ullman}, TITLE = {Introduction to Automata Theory, Languages and Computation}, PUBLISHER = aw, YEAR = 1979 } @book{ hopcroft/etal:2001, AUTHOR = {John E. Hopcroft and Rejeev Motwani and Jeffrey D. Ullman}, TITLE = {Introduction to Automata Theory, Languages and Computation}, PUBLISHER = aw, YEAR = 2001, EDITION = {2nd} } @article{ huizing/deroever:1991, AUTHOR = {C. Huizing and W.P. de Roever}, TITLE = {Introduction to design choices in the semantics of {Statecharts}}, JOURNAL = {Information Processing Letters}, YEAR = 1991, VOLUME = 37, PAGES = {205--213}, SUMMARY = {Nice and quick reading. Motivation for kind of synchrony hypothesis in statecharts. To be honest: not particularly inventive. The thing is obvious, but the paper tries to give a deeper motivation by drawing some properties of reactive system. In a way it derives the synchrony hypothesis from requirments on semantics.} } %%% I: @misc{ isoc:1999, TITLE={International Standard. {Programming} {Languages} - {C}}, NOTE={Ref. ISO/IEC 9899:1999(E)}, KEY={International} } %%% J: @inproceedings{ jansen:2002b, AUTHOR = {David N. Jansen}, TITLE = {Probabilistic {UML} Statecharts for Specification and Verification: a case study.}, CROSSREF = {CSDUML:2002} } @mastersthesis{ jacobsen:1999, AUTHOR = {Peter Jacobsen}, TITLE = {Code Generation for Embedded Systems}, SCHOOL = {Technical University of Denmark (Lyngby) and IT University of Copenhagen}, YEAR = 1999, MONTH = apr, SUMMARY = {Compiles VS flat State/Event system (before they had become more like real statecharts) using BDDs. The reaction relations are encoded in BDD and the BDD serves as runtime representation for the model. The runtime library boils down to implementation of fundamental BDD algorithms and wrapping these in a loop. Results are not very promising: BDD implementation is only smaller/faster for very few models. VS wins most often. One of the reasons might be that it has actually been applied only to flat models.} } @book{ jones/etal:1993a, AUTHOR = {Neil D. Jones and Carsten K. Gomard and Peter Sestoft}, TITLE = {Partial Evaluation and Automatic Program Generation}, PUBLISHER = ph, SERIES = isics, SUMMARY = {The Book on partial evaluation. Perhaps a bit outdated when you look for bleeding edge research in the area. Otherwise a solid introduction to the topic.}, NOTE = {\url{http://www.dina.kvl.dk/~sestoft/pebook}}, YEAR = 1993, } @comment{ :K } @article{kannan/etal:1992, AUTHOR = {S. Kannan and M. Naor and S. Rudich}, TITLE = {Implicit representation of graphs}, JOURNAL = {SIAM J. DISC. MATH.}, YEAR = 1992 } @inproceedings{kirsch:2002a, AUTHOR = {Christoph M. Kirsch}, TITLE = {Principles of Real-Time Programming}, CROSSREF = {EMSOFT:2002}, PAGES = {61--75}, SUMMARY = {It was a nice and general talk explaining the whole approach of making real time programming easier. Details may be find in earlier papers, especially in one on E-code (PLDI2002) and Giotto (EMSOFT01)} } @inproceedings{knapp/merz:2002, AUTHOR = {Alexander Knapp and Stephan Merz}, TITLE = {Model Checking and Code Generation for {UML} State Machines and Collaborations}, BOOKTITLE = {5th Workshop on Tools for System Design and Verification}, YEAR = 2002, PUBLISHER = {Institut f\"ur Informatik, Universit\"at Augsburg}, SERIES = {Technical Report 2002-11}, PAGES = {59--64}, EDITOR = {Dominik Haneberg and Gerhard Schellhorn and Wolfgang Reif}, SUMMARY = {A general paper describing the implementation of Hugo. Very similar to content of invited talk on CSDUML'02 by Stephan Merz. Introduces the idea of code generation to Java, which attempts to produce code very close to UML meta-model. Authors do take an effort to optimize representations presented to model-checkers (they use SPIN and UPPAAL), because verification time should be feasible for practical reasons. (BTW. The UPPAAL model is flattened). For some reason they do not consider execution efficiency as important, and generate Java code which seems completely unnaceptable for practical use (40 classess and 800 lines of code for tiny example).} } @comment{ :KN } @Book{knuth1997a, author = {Donald E. Knuth}, title = {The Art of Computer Programming}, publisher = aw, year = 1997, volume = 1, edition = {3rd.} } @comment :KO @misc{kowaltowski:1993, AUTHOR = {Tomasz Kowaltowski and Claudio L. Lucchesi and Jorge Stolfi}, TITLE = {Minimization of binary automata}, TEXT = {Technical Report Relat DCC-22/93, Departamento de Ciencia de Computacao, Universidade Estudual de Campinas.}, YEAR = 1993, URL = {citeseer.nj.nec.com/tomasz93minimization.html}, SUMMARY = {Motivation for usage binary automatas and looking for optimal order of transitions. A 'fold' heuristics is given for the problem, which apparently will work much worse for graphs containing cycles (also it is still possible to adopt it to cyclic graphs - I think). Also an encoding (storage representation) for graphs is given which is not going to be particularly useful in our case.}, } @comment :LA @inproceedings{ laleau/mammar:2000a, AUTHOR = {R{\'e}gine Laleau and Amel Mammar}, TITLE = {An overview of a method and its support tool for generating {B} specifications from {UML} notations}, PAGES = {269--272}, URL = {http://ieeexplore.ieee.org/iel5/7013/18910/00873675.pdf}, CROSSREF = {ASE:2000}, AWNO = 0032, AWBI = 005, SUMMARY = {Gives an overview of how UML model can be developed with B support, with automatic translation to B etc. Does not go into details on how the translation is done. This is supposed to be described in separate, inaccessible papers.} } @inproceedings{ lano/etal:2000a, AUTHOR = {Kevin Lano and Kelly Androutsopoulos and David Clark}, TITLE = {Structuring and Design of Reactive Systems Using {RSDS} and {B}}, BOOKTITLE = {Third International Conference Fundamental Approaches to Software Engineering (FASE)}, YEAR = 2000, PUBLISHER = sv, SERIES = lncs, VOLUME = 1783, ADDRESS = {Berlin, Germany}, PAGES = {97--111}, EDITOR = {T. S. E. Maibaum}, SUMMARY = {Apparently the main contribution is to give a structured way to design statecharts as replacement of ad hoc design. See lano/etal:200b for similar work with different case study. In my opinion this is really not about statecharts.}, AWBI = 005, AWNO = 0025 } @inproceedings{ lano/etal:2000b, AUTHOR = {Kevin Lano and David Clark and Kelly Androutsopoulos and Pauline Kan}, TITLE = {Invariant-Based Synthesis of Fault-Tolerant Systems}, BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant Systems, 6th International Symposium (FTRTFT)}, YEAR = 2000, MONTH = sep, PUBLISHER = sv, SERIES = lncs, ADDRESS = {Pune, India}, PAGES = {46--57}, EDITOR = {Mathai Joseph}, SUMMARY = {This paper presents SRS, a structured notation for statecharts and uses it for development of reactive systems. I find the notation extremely distant from actual statecharts. This is a set of flat state machines (a flat statechart) which have additional hierarchy described separately. The hierarchy is different than in statecharts; it could be called a hierarchy of subordination. A transition in given OR-state (called a Module) can only refer to subordinate states in guard and can only send events to subordinate modules (down the hierarchy). This concept of hierarchy seems rather rigid and artificial. Also there is no relation to statechart hierarchy whatsoever. The case study is fault tolerant production cell.}, AWBI = 005, AWNO = 0024 } @PhdThesis{larsen:1986a, author = {Kim G. Larsen}, title = {Context Dependent Bisumulation Between Processes}, school = {Edinburgh University}, year = 1986 } @comment{ article{0890540119929918623892620496, @Comment author = {Larsen, K.G. and Milner, R.}, @Comment journal = {Information and Computation}, @Comment volume = 99, @Comment number = 1, @Comment pages = {80-108}, @Comment year = 1992, @Comment ISSN = 08905401, @Comment abstract = {The authors illustrate a compositional proof method for communicating systems; that is, a method in which a property P of a complete system is demonstrated by first decomposing the system, then demonstrating properties of the subsystems which are strong enough to entail property P for the complete system. In any compositional proof method, it is essential that one can abstract away the behavioural aspects of the subsystem which are irrelevant in the context of the complete system. The authors' method is an extension of the well established notion of bisimulation; it is called relative bisimulation, and was developed specifically to allow for such abstractions. They illustrate the method in a proof of correctness for a version of the alternating bit protocol}, @Comment title = {A compositional protocol verification using relativized bisimulation} @Comment } } @comment :Le @inproceedings{ ledang:2001a, AUTHOR = {Hung Ledang}, TITLE = {Automatic Translation from {UML} Specifications to {B}}, BOOKTITLE = {16th IEEE International Conference on Automated Software Engineering (ASE)}, YEAR = 2001, MONTH = nov, PUBLISHER = ieee, ADDRESS = {San Diego, CA, USA}, PAGES = {436nn}, AWNO = 0029, AWBI = 005, SUMMARY = {A very superficial description on how rather complete UML specficiation can be translated to B method specification. As far as statecharts are concerned not much info is given (but see other papers). This seems to be published at least twice. This citation refers to phd thesis symposium of ASE. Exactly the same paper was apparently published at RCS'02 workshop in Grenoble.} } @inproceedings{ ledang/souquieres:2001a, AUTHOR = {Hung Ledang and Jeanine Souqui{\`e}res}, TITLE = {Formalizing {UML} Behavioral Diagrams with {B}}, BOOKTITLE = {Tenth {OOPSLA} Workshop on Behavioral Semantics: Back to Basics}, YEAR = 2001, MONTH = oct, ADDRESS = {Tampa Bay, Florida, USA}, AWNO = 0030, AWBI = 005, SUMMARY = {This paper does not give any interesting details about statecharts, despite the suggestive title.} } @inproceedings{ ledang/souquieres:2002a, AUTHOR = {Hung Ledang and Jeanine Souqui{\`e}res}, TITLE = {Contributions for Modelling {UML} State-Charts in {B}}, BOOKTITLE = {Third International Conference on Integrated Formal Methods (IFM)}, YEAR = 2002, PUBLISHER = sv, SERIES = lncs, VOLUME = 2335, ADDRESS = {Turku, Finland}, PAGES = {109--127}, EDITOR = {Michael J. Butler and Luigia Petre and Kaisa Sere}, AWNO = 0031, AWBI = 005 } % :LI @techreport{ lilius/paltor:1999, AUTHOR = {Johan Lilius and Iv\'an Porres Paltor}, TITLE = {The Semantics of {UML} State Machines}, YEAR = 1999, MONTH = may, INSTITUTION = {Turku Centre for Computer Science}, ADDRESS = {\`Abo Akademi University, Finland}, NUMBER = {No~273}, ISBN = {952-12-0446-X}, SUMMARY = {An interesting trial to make UML statecharts semantics formal. Some choices may seem to be unsuccesful but I used it as a basis for my formal semantics of visualSTATE.} } @phdthesis{ lind-nielsen:2000, AUTHOR = {J{\o}rn Bo {Lind Nielsen}}, TITLE = {Verification of Large/State Event Systems}, SCHOOL = {Technical University of Denmark}, YEAR = 2000, MONTH = apr, AWNO = 0049, AWBI = 006, } @article{ lind-nielsen/etal:2001, AUTHOR = {J. Lind-Nielsen and H. R. Andersen and H. Hulgaard and G. Behrmann and K. Kristoffersen and K. G. Larsen}, TITLE = {Verification of Large State/Event Systems using Compositionality and Dependency Analysis}, JOURNAL = {Formal Methods in System Design}, VOLUME = 18, NUMBER = 1, PAGES = {5--23}, MONTH = jan, YEAR = 2001, SUMMARY = {Contains the mathematical description of S/E (flat) visualSTATE model. Otherwise it's about BBDs and verification stuff.} } % :LY @inproceedings{lynch:1988a, AUTHOR = {Nancy Lynch}, TITLE = {{I/O} Automata: A model for discrete event systems}, BOOKTITLE = {Annual Conference on Information Sciences and Systems}, YEAR = {1988}, ADDRESS = {Princeton University, Princeton, N.J.}, PAGES = {29--38}, URL = {http://theory.lcs.mit.edu/tds/papers/Lynch/princeton88.pdf}, AWBI = 003, AWNO = 0042, SUMMARY = {Introduction to I/O automata, composition, fairness and implementation relation. Candy machines examples.} } @techreport{lynch/tuttle:1988a, AUTHOR = {Nancy A. Lynch and Mark R. Tuttle}, TITLE = {An Introduction to Input/Output Automata}, YEAR = 1988, MONTH = nov, INSTITUTION = mit, NUMBER = {MIT/LCS/TM-373}, SUMMARY = {An improved longer version of lynch:1988a, better typeset, more readable, proof methods are addde.}, AWBI = 003, AWNO = 0043 } % :MA @book{ magee/kramer:1999, AUTHOR = {Jeff Magee and Jeff Kramer}, TITLE = {Concurrency. State Models and Java Programs}, PUBLISHER = {John Wiley \& Sons}, ADDRESS = {Chichester}, YEAR = 1999, } @inproceedings{maraninchi:1991b, AUTHOR = {Florence Maraninchi}, TITLE = {The {Argos} Language: Graphical representation of automata and description of reactive systems}, BOOKTITLE = {IEEE Workshop on Visual Languages}, MONTH = oct, YEAR = 1991, ADDRESS = {Kobe, Japan}, URL = {http://www-verimag.imag.fr/~maraninx/IEEE-VISUAL91.html}, SUMMARY = {Introduction to Argos. Perhaps not very detailed. I have the impression that the only important differences from statecharts are simplified guards and no transitions crossing hierarchy levels. This means that Argos is actually very similar to VisualSTATE (except that VS transitions are general).} } @inproceedings{maraninchi/halbwachs:1996b, AUTHOR = {Florence Maraninchi and Nicolas Halbwachs}, TITLE = {Compiling {ARGOS} into Boolean Equations}, BOOKTITLE = {Proc. 4th Int. School and Symposium on Formal Techniques in Real Time and Fault Tolerant Systems (FTRTFT)}, YEAR = 1996, MONTH = sep, PUBLISHER = sv, SERIES = lncs, VOLUME = 1135, ADDRESS = {Uppsala, Sweden}, SUMMARY = {The semantics of argos is first given in terms of Mealy machine. Then a scheme is proposed to implictly represent this machine in an equation system. Gives some insight on DC format. I need more. I would like to know how DC incorporates arbitrary data types and external function calls. This could allow as to target DC platform and use Esterel compiler for statecharts. But beware. There is already a INRIA report on similar problem. Unfortunately states become explicit flows similarly like in Sehsia's translation of statecharts to Esterel. Still it seems this is a promising approach} } @inproceedings{ maraninchi/remond:2000, AUTHOR = {Florence Maraninchi and Yann R{\'e}mond}, TITLE = {Applying Formal Methods to Industrial Cases: The Language Approach (The Production-Cell and Mode-Automata)}, BOOKTITLE = {5th International Workshop on Formal Methods for Industrial Critical Systems (FMICS)}, YEAR = 2000, MONTH = apr, ADDRESS = {Berlin,Germany}, SUMMARY = {Describes extension of Lustre with modes (based on Mode-automata). The case example is the Production Cell. The paper improves on code generation comparing to normal Lustre.}, AWBI = 007, AWNO = 0016 } @article{ maraninchi/remond:2001, AUTHOR = {Florence Maraninchi and Yann R{\'e}mond}, TITLE = {{Argos}: an automaton-based synchronous language}, JOURNAL = {Computer Languages}, YEAR = 2001, VOLUME = 27, NUMBER = {1--3}, PAGES = {61--92}, URL = {http://www.elsevier.com/gej-ng/10/15/18/54/27/31/abstract.html}, SUMMARY = {Nice fully fledged introduction to Argos and its semantics. Good theoretical motivation. Note that the URL above only points to the abstract. Subscription to Science Direct is needed to get the full text.}, ISSN = {0096-0551}, PUBLISHER = esp } @book{marwedel/goosens:1995, AUTHOR = {Peter Marwedel and Gert Goosens}, TITLE = {Code Generation for Embedded Processors}, PUBLISHER = kap, ADDRESS = {Boston/London/Dordrecht}, YEAR = 1995, } %popraw to na inbook @misc{ marwedel:1995, AUTHOR = {Peter. Marwedel}, TITLE = {Code Generation for Embedded Processors: An Introduction}, NOTE = {Introductory article in book: Code Generation for Embedded Processors}, YEAR = 1995, PAGES = {14--31}, PUBLISHER = kap, SUMMARY = {Describes general issues of code generation for embedded systems. I liked the remarks on timed systems and time constraints verified code. Also explains briefly the idea of optimal coverages and referes to many chapters in the book wich may proof to be relevant. I have it printed - do not have the book yet. IT MAY BE USEFUL TO REVIEW THE BIBLIOGRAPHY ONCE AGAIN.} } @article{meinel/stangier:2001, AUTHOR = {Christoph Meinel and Christian Stangier}, TITLE = {Data Structures for Boolean Functions. {BDDs} -- Foundations and Application}, JOURNAL = lncs, YEAR = 2001, VOLUME = 2122, PAGES = {61--78}, SUMMARY = {General description of ROBDDS and operation on them. Not very detailed. Example of verification of FSM equivalence. Something about strategies for variable ordering. Quite big bibliography. Notes on currect research -- different modified versions of BBDs}, } @inproceedings{meur/consel:2000a, AUTHOR = {Anne-Francoise {Le Meur} and Charles Consel}, TITLE = {Generic Software Component Configuration via Partial Evaluation}, BOOKTITLE = {Workshop on Product Line Architecture}, YEAR = 2000, MONTH = aug, ADDRESS = {Denver, USA}, SUMMARY = {A preliminary presentation of the language for defining specialization oportunities for modules ad combining them into programs.}, AWBI = 002, AWNO = 0010, } %%% :MI @Book{milner:1989a, author = {Robin Milner}, title = {Communication and Concurrency}, publisher = ph, year = 1989, series = ph-cs, } @inproceedings{mikk/etal:1997, AUTHOR = {Erich Mikk and Yassine Lakhnech and Michael Siegel}, TITLE = {Hierarchical Automata as Model for Statecharts}, BOOKTITLE = {Third Asian Computing Science Conference (ASIAN)}, YEAR = 1997, MONTH = dec, PUBLISHER = sv, SERIES = lncs, VOLUME = 1345, ADDRESS = {Kathmandu, Nepal}, PAGES = {181--196}, EDITOR = {R. K. Shyamasundar and Kazunori Ueda}, SUMMARY = {Describes EHA (extended HA) as a simpler, but still compact language for representing statecharts internally in the tools. This language has a simpler semantics and could be used as intermediate format for various translators (model checkers and code generators). The size of EHA wrt to size of source statechart seems to be OK (polynomial), but there is no explanation on how other language features like history are treated (which may influence the size significantly). Apart from that the description is rather comprehensible.}, AWBI = 006, AWNO = 0020 } @inproceedings{mikk/etal:1998, AUTHOR = {Erich Mikk and Yassine Laknech and Michael Siegel and Gerard J. Holzmann}, TITLE = {Implementing statecharts in {PROMELA}/{SPIN}}, BOOKTITLE = {2nd IEEE Workshop on Industrial Strength Formal Specification Techniques}, YEAR = 1998, MONTH = oct, ADDRESS = {Boca Raton, Florida}, PAGES = {90--101}, PUBLISHER = ieee, AWBI = 006, AWNO = 0045, SUMMARY = {Translation of Statecharts to PROMELA, using Extended Hierarchical Automata (EHA) by the same authors as an intermediate format. The first stage of the translation (statecharts->EHA) is not described, but it seems to be fairly straightforward. In principle EHA is an interesting intermediate format, which could be considered for code generation also. It should have simpler runtime semantics than my Absyn model (described in wasowski:2003a). The translation from EHA to PROMELA is claimed to be compositional, which is needed to verify the correctness of generated code. Automata theoretic approach of SPIN (as for 98) was not too successful for this application. One cannot expect big models to be verifiable. Authors had intended to try symboli methods in following work.}, AWBI = 006, AWNO = 0018, URL = {http://ieeexplore.ieee.org/iel5/6218/16603/00766303.pdf} } %%% :MO @phdthesis{ moeller:2002, AUTHOR = {Jesper B. M{\o}ller}, TITLE = {Symbolic Model Checking of Real-Time Systems Using Difference Decision Diagrams.}, SCHOOL = {Department of Innovation, \hbox{IT University} of Copenhagen}, MONTH = apr, YEAR = 2002, SUMMARY = {model checking of real time systems specified with language of guarded commands. DDDs as data structure for formulas containing time differences -- designed after BDDs.} } @misc{ mof:2002, AUTHOR = {{Object Management Group}}, TITLE = {Meta Object Facility ({MOF}) Specification}, YEAR = 2002, URL = {\url{http://www.omg.org/technology/documents/formal/mof.htm}}, NOTE = {\url{http://www.omg.org}} } @comment{ --- :MU } @misc{ muddy, AUTHOR = {Ken {Friis Larsen} and Jakob Lichtenberg}, TITLE = {{MuDDy} 2.0 -- {SML} Interface to the Binary Decision Diagrams Package {BuDDy}}, NOTE = {\url{http://www.itu.dk/research/muddy}}, URL = {\url{http://www.itu.dk/research/muddy}}, SUMMARY = {BDD library implemented in C (fast) but accessible from MoscowML programs} } @InProceedings{murakami:1995a, author = {Masaki Murakami}, title = {Partial Evaluation of Reactive Communciating Processes using Temporal Logic Formulas}, booktitle = {Workshop on Algebraic and Object-Oriented Approaches to Software Science}, year = 1995, summary = {TODO}, awno = 0050, awbi = 002 } @comment{ --- :NI } @inproceedings{niaz/tanaka:2003a, AUTHOR = {Iftikhar Azim Niaz and Jiro Tanaka}, TITLE = {Code Generation from {UML} Statecharts}, BOOKTITLE = {7th IASTED International Conference on Software Engineering and Applications (SEA 2003)}, YEAR = 2003, MONTH = nov, ADDRESS = {Marina del Rey, CA, USA}, AWBI = 005, AWNO = 0047, SUMMARY = {The paper describes a translation from statecharts to Java. Methods are used to encode transitions in a very standard way (I would say). They seem to compare their technique agains "standard" nested switch sequences, disregarding the fact that (1) they were standard may be 10 years ago and (2) what they do is not very different because the switch is still made, except it happens in the byte code generated by the compiler. Hardly any efficiency gain can be expected. They do not comment on efficiency, but emphasize the readability of the code. A very similar paper to ali/tanaka:1999. I cannot really figure out what is the main difference. The related work section is also rather poor commenting only on a small fraction of code generation appraoches available.}, URL = {http://www.iplab.is.tsukuba.ac.jp/paper/international/niaz_sea2003.pdf} } %%% :NO @book{noble/weir:2001, AUTHOR = {James Noble and Charles Weir}, TITLE = {Small Memory Software. Patterns for systems with limited memory}, PUBLISHER = aw, YEAR = 2001, } %%% :OM @misc{ omg:1999, AUTHOR = {{Object Management Group}}, TITLE = {{OMG} {Unified} {Modelling} {Language} Specification}, YEAR = 1999, SUMMARY = {I only printed the part on state charts semantics and notation. The whole text is above 800 pages}, URL = {\url{http://www.omg.org/technology/documents/formal/uml.htm}}, NOTE = {\url{http://www.omg.org}} } @article {parnas:1976a, AUTHOR = {David L. Parnas}, TITLE = {On the Design and Development of Program Families}, JOURNAL = tose, YEAR = 1976, MONTH = mar, VOLUME = {Vol. SE-2}, NUMBER = {No. 1}, PAGES = {1--9}, SUMMARY = {Presumably a very classic paper which introduces one of the fundamental concepts that programmers use in everyday life noweday: information hiding, interfaces and modules. The title sounds a bit like "generative programming thing" and GP people like to refer to it, but I do not think that there is anything specifically generative in it. Actually it says that it is orthogonal to program generation.}, } @inproceedings{ pnueli/etal:1998, AUTHOR = {Amir Pnueli and M. Siegel and O. Shtrichman}, TITLE = {The {Code} {Validation} {Tool} ({CVT}) -- {Automatic} verification of code generated from synchronous languages.}, BOOKTITLE = {The International Workshop on Software Tools for Technology Transfer}, YEAR = 1998, MONTH = jul, PUBLISHER = {BRICS}, VOLUME = {NS-98-4}, SERIES = {BRICS notes series}, ADDRESS = {Aalborg, Denmark}, PAGES = {7--12}, SUMMARY = {High level description of CVT tool - Code Validation Tool. This tool was implemented us part of the huge SACRES development framework. It aims at proving correctness of code generated automatically from STATEMATE and SILDEX models. Apparently it only proves the correctness of last step: translation of DC+ into C. This is done by abstractions over functions and various technical tricks to reduce the time needed for verification. It seems that reasonably big examples can be proven this way. Apparently it combines model-checking and transformational proofs. Details of code generation are not diclosed (they refer to industrial implementation). } } @inproceedings{ pnueli/shalev:1991, AUTHOR = {Amir Pnueli and M. Shalev }, TITLE = {What is in a Step: On the Semantics of Statecharts}, BOOKTITLE = {International Conference on Theoretical Aspects of Computer Software (TACS)}, YEAR = {Septmeber 24-27, 1991}, MONTH = sep, ADDRESS = {Sendai, Japan}, PUBLISHER = sv, SERIES = lncs, VOLUME = 526, PAGES = {244--264}, EDITOR = {Takayasu Ito and Albert R. Meyer}, ISBN = {ISBN 3-540-54415-1}, SUMMARY = {Operational and declarative semantics of statecharts, but different than the one given originally by Harel/etal. I particularly like this paper for its clarity, density and that it corrected severl minor bugs and inconsistenties of harel/etal. Still it seems that some semantic choices "in the step" may not be very relevant for visual STATE implementation.} } @comment { :RA } @InProceedings{rajamani/rehof:2002a, author = {Sriram K. Rajamani and Jakob Rehof}, title = {Conformance Checking for Models of Asynchronous Message Passing Software}, crossref = {CAV:2002}, pages = {166--179}, awbi = 006, awno = 0054 } @inproceedings{ ramesh:1999a, AUTHOR = {S. Ramesh}, TITLE = {Efficient Translation of Statecharts into Hardware Circuits}, BOOKTITLE = {12th International Conference on VLSI Design}, YEAR = 1999, MONTH = jan, PUBLISHER = ieee, PAGES = {384--389}, AWNO = {005/0007} } % :RH @misc{ rhapsodyinuc, AUTHOR = {{I-Logix Inc.}}, TITLE = {{Rhapsody\ensuremath{^\text{\textregistered}}} in {MicroC}}, NOTE = {http://www.ilogix.com}, URL = {http://www.ilogix.com} } % :RI @inproceedings{ riebisch/etal:2002a, AUTHOR = {Matthias Riebisch and Ilka Philippow and Marco G{\"o}tze}, TITLE = {{UML}-Based Statistical Test Case Generation}, BOOKTITLE = {Objects, Components, Architectures, Services, and Applications for a Networked World. NetObjectDays, Revised Papers}, YEAR = 2002, MONTH = oct, PUBLISHER = sv, SERIES = lncs, VOLUME = 2591, ADDRESS = {Erfurt, Germany}, PAGES = {394--411}, EDITOR = {Mehmet Aksit and Mira Mezini and Rainer Unland}, SUMMARY = {This paper is of interest because it uses statechart transformations which are also applied in code generation. This paper flattens and expands (to product machines) statecharts to transform them into usage graphs. This graphs are then used to generate usage tests. The paper admits that their flattening approach blows up and makes test-cases unmanageable for bigger models.}, AWBI = {004}, AWNO = {0038} } % :RO @misc{ rosert, AUTHOR = {{Rational Software Corp.}}, TITLE = {{Rational Rose\ensuremath{^\text{\textregistered}} Real Time (RoseRT)}}, NOTE = {http://www.rational.com/products/rosert/}, URL = {http://www.rational.com/products/rosert/}, } @inproceedings{ roubtsova/etal:2001, AUTHOR = {Ella E. Roubtsova and Jan van Katwijk and Ruud C. M. de Rooij and Hans Toetenel}, TITLE = {Transformation of {UML} Specification to {XTG}}, BOOKTITLE = {Perspectives of System Informatics (PSI), 4th International Andrei Ershov Memorial Conference, Revised Papers}, YEAR = 2001, MONTH = jul, PUBLISHER = sv, SERIES = lncs, VOLUME = 2244, ADDRESS = {Akademgorodok, Novosibirsk}, PAGES = {249--256}, EDITOR = {Dines Bj{\o}rner and Manfred Broy and Alexandre V. Zamulin}, URL = {http://link.springer.de/link/service/series/0558/bibs/2244/22440247.htm}, ISBN = {3-540-43075-X}, SUMMARY = {Another translation of statecharts (and only slightly more than statecharts) to model checker's language (XTG). The translation starts with flattening and wins by using channel communication for cascades which avoids explosion. This is however not flattening statecharts to statecharts, but flat statecharts with CCS channels. Extremely clumsy notation makes understanding of the examples hard.}, AWBI = 006, AWNO = 0021 } @book{ rozenberg/salomaa:1997, EDITOR = {G. Rozenberg and A. Salomaa}, TITLE = {Handbook of Formal Languages}, PUBLISHER = sv, YEAR = 1997, VOLUME = 3, SUMMARY = {A third part of 3 volume compendium on formal languages. This one devotes some parts to traces, etc.}, AWNOTE = {Expensive. ITU has a copy in reference library. I do not have it} } % :SA @inproceedings {sawa:2003a, AUTHOR = {Zdenek Sawa}, TITLE = {Equivalence checking of non-flat systems is {EXPTIME}-hard}, BOOKTITLE = {International Conference on Concurrency Theory (CONCUR)}, YEAR = 2003, MONTH = sep, EDITOR = {FIXME}, PUBLISHER = sv, SERIES = lncs, ADDRESS = {Marseille, France}, PAGES = {FIXME}, SUMMARY = {The paper discusses complexity of equivalence checking for non-flat systems. Not that interesting for me as non-flat systems are understood as systems with structure. So called "flat" comunicating state machines fall well into this category. (have not got a copy)} } % :SC @misc{ scope, TITLE = {{SCOPE}: {A} statechart compiler}, KEY = {scope}, NOTE = {\hbox{\url{http://www.mini.pw.edu.pl/~wasowski/scope}}}, URL = {\hbox{\url{http://www.mini.pw.edu.pl/~wasowski/scope}}}, YEAR = 2003, } @techreport{ scott/ramsey:2000, AUTHOR = {Kevin Scott and Norman Ramsey}, TITLE = {When Do Match-compilation Heuristics Matter?}, YEAR = 2000, MONTH = may, INSTITUTION = {Department of Computer Science, University of Virginia}, NUMBER = {CS-2000-13}, SUMMARY = {Survey and experimental comparison of match compilation methods. This paper is somewhat relevant to statechart implementation problem, as it discusses heuristics to build cheap decision trees. Similar problem should probably be addressed by a more advanced statechart code generator (when building the mechanism for selecting enable transitions). }, } % :SE @inproceedings{ sekerinski:1998a, AUTHOR = {Emil Sekerinski}, TITLE = {Graphical Design of Reactive Systems}, BOOKTITLE = {Second International B Conference. Recent Advances in the Development and Use of the B Method}, YEAR = 1998, MONTH = apr, PUBLISHER = sv, SERIES = lncs, VOLUME = 1393, ADDRESS = {Montpellier, France}, PAGES = {182--197}, EDITOR = {Didier Bert}, AWNO = 0028, AWBI = 005, SUMMARY = {A paper very similar to sekerinski/zurob:2001 and sekerinski/zurob:2002a. The main focus is on how statecharts are translated to AMN B. The next paper focuses slightly more on tool overview, while the last formalizes algorithms. In principle all three vastly overlap (AFAICS) and could be made one paper easily to benefit of everybody.} } % nie zmieniaj klucza, bo sa juz odwolania... @inproceedings{ sekerinski/zurob:2001, AUTHOR = {Emil Sekerinski and Rafik Zurob}, TITLE = {{iState}: A Statechart Translator}, crossref = {UML:2001}, PAGES = {376--390}, SUMMARY = {Rather superficial description of translation scheme for UML state charts. Target language is B notation. Set notation is used to express some properties which I find succint and nice (it takes some time to get used to it though). Models are without history. This is not efficiency or code size oriented. In contrary the focus is on readable code...}, AWNO = 0026, AWBI = 005 } @inproceedings{ sekerinski/zurob:2002a, AUTHOR = {Emil Sekerinski and Rafik Zurob}, TITLE = {Translating Statecharts to {B}}, BOOKTITLE = {Third International Conference on Integrated Formal Methods (IFM)}, YEAR = 2002, MONTH = may, PUBLISHER = sv, SERIES = lncs, ADDRESS = {Turku, Finland}, PAGES = {128--144}, EDITOR = {Michael J. Butler and Luigia Petre and Kaisa Sere}, SUMMARY = {Describes the translation process of iState tool overviewed in sekerinski/zurob:2001. Statecharts are translate to Abstract Machine Notation of B method (AMN B). Entry/exit actions and history states are not considered (they mention it explicitly). There is no flattening involved (translation is to nested hierarchy of case statements and concurrent compositions of AMN). The resulting code relatively nicely reflects the original statechart. Proper targets are computer which yields a polynomial growth of the model (in number of states times number of transitions). Current active state of each machine is kept in a variable, but no special value is used for idle state (as in my flattening). Consequently guard conditions have to be flattened by closure upto the root of the hierarchy, exactly as in my flattening. This yields an increase of model size in depth of the model and maximal number of guards, though it is acceptable and can be treated as polynomial. The paper is well written and clear. It is also a bit stronger technically than the 2001 version.}, AWNO = 005, AWBI = 0027 } @inproceedings{ seshia/etal:1999, AUTHOR = {S.A.Seshia and R.K. Shyamasundar and A.K. Bhattacharjee and S.D. Dhodapkar}, TITLE = {A Translation of Statecharts to {Esterel}}, BOOKTITLE = {FM'99 - Formal Methods, World Congress on Formal Methods in the Development of Computing Systems}, YEAR = 1999, MONTH = sep, PUBLISHER = sv, SERIES = lncs, ADDRESS = {Toulouse, France}, VOLUME = {1709}, PAGES = {983--1007}, EDITOR = {Jeannette M. Wing and Jim Woodcock and Jim Davies}, URL = {http://www.tcs.tifr.res.in/~shyam/safecomp99.ps}, SUMMARY = {Finally something close to my work. Not so much focus on efficiency. The aim was to generate verifiable code and use esterel model checkers. Code size/speed results remain unknown. I do not quite agree that there are not many tools for verifying statecharts. The feeling is actually that one may do more for statecharts than for Esterel itself.} } % :SI @inproceedings{ siegel/etal:1997, AUTHOR = {E. Mikk and Y. Lakhnech and C. Petersohn and M. Siegel}, TITLE = {On Formal Semantics of Statecharts as Supported by {STATEMATE}}, BOOKTITLE = {2nd BCS-FACS Northern Formal Methods Workshop}, YEAR = 1997, PUBLISHER = sv, URL = {http://citeseer.nj.nec.com/mikk97formal.html}, SUMMARY = {A counterpart to Harel and Naamad. Aims to express the same but formally. Unfortunately uses Z notation and does not support history states. Guards are limited in similar way as it was in old-good-flat visualSTATE.} } @inproceedings{ simons:2000a, AUTHOR = {Anthony J. H. Simons}, TITLE = {The compositional properties of {UML} statechart diagrams}, BOOKTITLE = {Third Electronic Workshop on Rigorous Object-Oriented Methods}, PUBLISHER = {British Computer Society}, EDITOR = {C. J. van Rijsbergen}, YEAR = 2000, URL = {citeseer.nj.nec.com/simons00compositional.html}, AWBI = 004, AWNO = 0037, SUMMARY = {Another proposal to "denastify" statecharts. Quite interesting, also some requirements seem to be slightly to strong (for instance level crossing transitions seem to be tractable by model-checking tools -- but OK since he seems to accept cross-level transitions, only insisting that tools should not deal with them, but only with the expanded versions. This partly confirms my experience with flattining). Interestingly (with good arguments) Simons advocates Harel's rule for conflict resolution as preserving dynamic compositionality.} } % :ST @article{ staunstrup/etal:2000, AUTHOR = {J{\o}rgen Staunstrup and Henrik Reif Andersen and Henrik Hulgaard and J{\o}rn Lind-Nielsen and Kim Guldstrand Larsen and Gerd Behrmann and Kaare J. Kristoffersen and Arne Skou and Henrik Leerberg and Niels Bo Theilgaard}, TITLE = {Practical Verification of Embedded Software}, JOURNAL = ieeec, YEAR = 2000, VOLUME = 5, NUMBER = 33, PAGES = {68--75}, SUMMARY = {This describes CBR technique for flat models. Hierarchy is mentioned in the end as an obstacle, which may be turned into real efficiency gain (if exploited).}, AWBI = 006, AWNO = 0014 } % :TA @article{ tarjan/etal:1979, AUTHOR = {Robert Endre Tarjan and Andrew Chi-Chih Yao}, TITLE = {Storing a Sparse Table}, JOURNAL = comm, YEAR = 1979, VOLUME = 22, NUMBER = 11, PAGES = {606--611}, SUMMARY = {double displacement as method to compress read only sparse tables with very good complexity results. May become useful where looking for final encoding.} } % :TI @article{ tip:1995a, AUTHOR = {Frank Tip}, TITLE = {A Survey of Program Slicing Techniques}, JOURNAL = {Journal of Programming Languages}, YEAR = 1995, MONTH = sep, VOLUME = 3, NUMBER = 3, PAGES = {121--189}, SUMMARY = {Probably the most comprehensive survey of slicing techniques.}, AWBI = 006, AWNO = 0004 } % :TO @inproceedings{ toetenel/etal:2001, AUTHOR = {Hans Toetenel and Ella Roubtsova and Jan van Katwijk}, TITLE = {A Timed Automata Semantics for Real-Time {UML} Specifications}, BOOKTITLE = {IEEE Symposia on Human-Centric Computing Languages and Environments}, YEAR = 2001, MONTH = sep, PUBLISHER = ieee, ADDRESS = {Stresa, Italy}, PAGES = {88--95}, URL = {http://ieeexplore.ieee.org/iel5/7811/21467/00995243.pdf}, SUMMARY = {This is a better version of roubtsova/etal:2001. Same authors, reordered though. This presentation is more complete, uses better notation and better language. In fact it looks like the previous paper was a draft of this one. There are not any significant differences, except for presentation quality.}, AWBI = 006, AWNO = 0022 } @book{ tofte:1990, AUTHOR = {Mads Tofte}, TITLE = {Compiler Generators - What They Can Do, What They Might Do and What They Probably Never Do}, PUBLISHER = sv, YEAR = 1990, VOLUME = 19, SUMMARY = {Contains a description of the CERES Compiler Generator and other systems. CERES was developed by Neil Jones and Mads Tofte.}, KEYWORDS = {compiler generation, CERES} } @unpublished{ tofte:1991, AUTHOR = {Mads Tofte}, TITLE = {Code Generation using Standard {ML}}, YEAR = 1991, SUMMARY = {These notes describe a compilation from the language PL/O to various abstract machines. Flow-of-control is handled using static {\bf continuations}. Register allocation is done using {\bf requirement maps}, a concept based on Hoare-triples. Lecture notes, not available online. ask Mads. NO CLUE HOW TO GET IT}, NOTE = {Probably never published and unobtainable} } % :TR @article{ traore:2000, AUTHOR = {Issa Traor\'e}, TITLE = {An Outline of {PVS} Semantics for {UML} Statecharts}, JOURNAL = {Journal of Universal Computer Science}, YEAR = 2000, VOLUME = 6, NUMBER = 11, PAGES = {1088--1108}, SUMMARY = {Describes semantics for statecharts using PVS. Perhaps would be more readble and reusable if not the PVS limitations and syntax} } % :TS @article{ tsakalidis:1984, AUTHOR = {A. K. Tsakalidis}, TITLE = {Maintaing order in a generalized linked list}, JOURNAL = {Acta Informatica}, YEAR = 1984, VOLUME = 21, NUMBER = 1, PAGES = {101--112}, AWBI = 005, AWNO = 0009 } % :VI @misc{ visualstate, AUTHOR = {{IAR Inc.}}, TITLE = {{IAR visualSTATE\ensuremath{^\text{\textregistered}}}}, NOTE = {\url{http://www.iar.com/Products/VS/}}, URL = {http://www.iar.com/Products/VS/} } % :VS @misc{ vsconceptguide, AUTHOR = {{IAR Inc.}}, TITLE = {{IAR visualSTATE\ensuremath{^\text{\textregistered}}} Concept Guide}, YEAR = 1999, NOTE = {Part of visualSTATE standard documentation} } @misc{ vsuserguide, AUTHOR = {{IAR Inc.}}, TITLE = {{IAR visualSTATE\ensuremath{^\text{\textregistered}}} User Guide}, YEAR = 2000, MONTH = oct, NOTE = {Part of visualSTATE standard documentation} } @misc{ vsrefguide, AUTHOR = {{IAR Inc.}}, TITLE = {{IAR visualSTATE\ensuremath{^\text{\textregistered}}} Reference Guide}, YEAR = 2000, MONTH = dec, NOTE = {Part of visualSTATE standard documentation} } @Unpublished{ vsrulebase40, AUTHOR = {M. Larsen}, COMPANY = {{IAR visualSTATE}}, YEAR = 1998, REVISION = {0.27}, TITLE = {{VisualSTATE} Rule Base 4.0 Specification ({IAR Inc.})}, NOTE = {Internal Document of IAR Inc.}, SUMMARY = {Incomplete, inconsistent, not-up-to date informal description of visualSTATE rulebase files. Still contains several unimplemented features. Overkilling detail level -- lexical structures described within grammar together with syntax. Covered by non-disclosure agreement. May only be obtained from IAR Inc. with their permission.} } @comment{ :WA } @techreport{ wang/etal:2000, AUTHOR = {Yunming Wang and Jean-Pierre Talpin and Albert Benveniste and Paul Le Guernic}, TITLE = {Pre-Order Semantics of {UML} State-Machines}, YEAR = 2000, MONTH = jun, INSTITUTION = {INRIA}, NUMBER = {No~3958}, ISSN = {0249-6399}, SUMMARY = {A mature approach to semantics of state charts. Includes history states. Especially I like the clean (and compact) approach of defining the structure and transitions. I belive I could use that in mine description} } @book{ warmer/kleppe:1999, AUTHOR = {Jos Warmer and Anneke Kleppe}, TITLE = {The Object Constraint Language. Precise Modelling with UML.}, PUBLISHER = aw, YEAR = 1999, SUMMARY = {A short and clear reading on OCL (about 80 pages of main content). It seems that OCL is not going to be implemented in SCOPE very soon, but admitably it is an interesting proposal} } @techreport{ wasowski/sestoft:2002a, AUTHOR = {Andrzej W{\k a}sowski and Peter Sestoft}, TITLE = {On the Formal Semantics of {visualSTATE} statecharts}, YEAR = 2002, MONTH = sep, INSTITUTION = {IT University of Copenhagen}, NUMBER = {TR-2002-19}, ISBN = {87-7949-026-3}, SUMMARY = {Implementation oriented precise operational semantics of {visualSTATE} statecharts}, } % FIXME: TU BRAKUJE POLSKIE LITERY W MOIM NAZWISKU @inproceedings{ wasowski/sestoft:2002b, AUTHOR = {Andrzej W{\k a}sowski and Peter Sestoft}, TITLE = {Compile-time Scope Resolution for Statecharts Transitions}, PAGES = {133--145}, CROSSREF = {CSDUML:2002} } @inproceedings{ wasowski:2003a, AUTHOR = {Andrzej W{\k a}sowski}, TITLE = {{On Efficient Program Synthesis from Statecharts}}, BOOKTITLE = {ACM SIGPLAN Languages, Compilers, and Tools for Embedded Systems (LCTES)}, YEAR = 2003, MONTH = jun, PUBLISHER = acm, ADDRESS = {San Diego, USA} } @InProceedings{ wasowski:2004a, author = {Andrzej W{\k a}sowski}, title = {{On Succinctness of Hierarchical State Diagrams in Absence of Message Passing}}, crossref = {SFEDL:2004} } @InProceedings{ wasowski:2004b, author = {Andrzej W{\k a}sowski}, title = {{Flattening Statecharts without Explosions}}, crossref = {LCTES:2004} } @InProceedings{ wasowski:2004c, author = {Andrzej W{\k a}sowski}, title = {Automatic Generation of Program Families by Model Restrictions}, crossref = {SPLC:2004}, note = {Accepted}, } % :WI @article{ wirth:1988, AUTHOR = {Niklaus Wirth}, TITLE = {The programming language {Oberon}}, JOURNAL = {Software -- Practice and Experience}, YEAR = 1988, MONTH = jul, VOLUME = 18, NUMBER = 7, PAGES = {671--690}, SUMMARY = {Only skim-read. I have an impression that nowadays most (all O-O) languages incorporate concepts of Oberon. Its only advantage would be to actually support type extensions (inheritance) without the whole oo machinery (classes)} } @inproceedings{ wirth:2001, AUTHOR = {Niklaus Wirth}, TITLE = {Embedded Systems and Real-Time Programming}, CROSSREF = {EMSOFT:2001}, PAGES = {486--492}, SUMMARY = {A general talk on properties and parctices of embedded software. Slightly conservative, but in the spirit I very much admire. Describes briefly an already-classic case study of helicopter control system. No direct relation to statecharts but advocates single threaded execution.} } % :XM @misc{ xmi:2002, AUTHOR = {{Object Management Group}}, TITLE = {{OMG} {XML} Metadata Interchange ({XMI}) Specification}, YEAR = 2002, MONTH = jan, URL = {http://www.omg.org/technology/documents/formal/xmi.htm}, NOTE = {http://www.omg.org} } % :ZI @InProceedings{ziadi/etal:2003a, title = {Product Line Derivation with {UML}}, booktitle = {Software Variability Management Workshop}, address = {University of Groningen Departement of Mathematics and Computing Science}, author = {Tewfik Ziadi and Jean-Marc J\'ez\'equel and Fr\'ed\'eric Fondement}, year = 2003, month = Feb, awno = 0053, awbi = 002 } % :ZU @unpublished{zundorf:2000, AUTHOR = {Albert Z\"undorf}, TITLE = {Rigorous Object Oriented Software Development with {Fujaba}}, NOTE = {Unpublished Draft}, YEAR = 2000, SUMMARY = {shorter version of Albert's habilitation. Incomplete as for 15/10/02} } @comment{ --- Workshop and Conference entries} % ::AS @proceedings{ ASE:2000, ORGANIZATION = {IEEE}, KEY = {IEEE}, TITLE = {Fifteenth IEEE International Conference on Automated Software Engineering (ASE)}, BOOKTITLE = {Fifteenth IEEE International Conference on Automated Software Engineering (ASE)}, PUBLISHER = ieee, ADDRESS = {Grenoble, France}, YEAR = 2000, MONTH = sep } @comment{ ::CA } @Proceedings{ CAV:2002, title = {14th International Conference on Computer Aided Verification (CAV)}, year = 2002, booktitle = {14th International Conference on Computer Aided Verification (CAV)}, editor = {Ed Brinksma and Kim Guldstrand Larsen}, volume = 2404, series = lncs, address = {Copenhagen, Denmark}, month = jul, publisher = sv } @comment{ ::CS } @proceedings{ CSDUML:2002, TITLE = {pUML Group Workshop on Critical Systems Development with {UML} ({CSDUML})}, BOOKTITLE = {pUML Group Workshop on Critical Systems Development with {UML} ({CSDUML})}, EDITOR = {Jan J{\"u}rjens and Maria Victoria Cengarle and Eduardo B. Fernandez and Bernhard Rumpe and Robert Sandner}, YEAR = 2002, MONTH = sep, PUBLISHER = {Technical University of Munich}, ADDRESS = {Dresden, Germany}, NOTE = {TUM-I0208}, AWNOTE = {have hardcopy} } @comment ::DA @Proceedings{danvy/etal:1996a, editor = {Olivier Danvy and Robert Gl{\"u}ck and Peter Thiemann}, year = 1996, month = feb, address = {Dagstuhl Castle, Germany}, title = {Partial Evaluation}, booktitle = {Partial Evaluation}, publisher = sv, series = lncs, volume = 1110, summary = {Partial Evaluation has reached a point where theory and techniques have matured, substantial systems have been developed, and realistic applications can benefit from partial evaluation. The 24 strictly refereed full papers included evaluate the progress achieved in the field during the last decade. Also included is a detailed preface by the volume editors and a subject index. All in all, this book competently reports the state of the art and future perspectives in partial evaluation.} } % ::EM @proceedings{ EMSOFT:2001, TITLE = {First International Workshop on Embedded Software ({EMSOFT})}, BOOKTITLE = {First International Workshop on Embedded Software ({EMSOFT})}, EDITOR = {Thomas A. Henzinger and Christoph M. Kirsch}, YEAR = 2001, MONTH = oct, PUBLISHER = sv, SERIES = lncs, VOLUME = 2211, ADDRESS = {Tahoe City, CA, USA}, AWNOTE = {have hardcopy} } @proceedings{ EMSOFT:2002, TITLE = {2nd International Conference on Embedded Software ({EMSOFT})}, BOOKTITLE = {2nd International Conference on Embedded Software ({EMSOFT})}, EDITOR = {Alberto Sangiovanni-Vincentelli and Joseph Sifakis}, YEAR = 2002, MONTH = oct, PUBLISHER = sv, SERIES = lncs, VOLUME = 2491, ADDRESS = {Grenoble,France}, AWNOTE = {have a hardcopy} } @comment{ ::LC } @Proceedings{ LCTES:2004, booktitle = {{ACM SIGPLAN Languages, Compilers, and Tools for Embedded Systems (LCTES)}}, title = {{ACM SIGPLAN Languages, Compilers, and Tools for Embedded Systems (LCTES)}}, year = 2004, month = jun, publisher = acm, address = {Washington DC, USA} } @comment{ ::SF } @Proceedings{ SFEDL:2004, booktitle = {{Workshop on Semantic Foundations of Engineering Design Languages (SFEDL)}}, title = {{Workshop on Semantic Foundations of Engineering Design Languages (SFEDL)}}, year = 2004, editor = {Michael Mendler}, publisher = esp, note = {Accepted. To be published in ENTCS} } @comment{ ::SP } % FIXME: change key for editor once it is known. Add volume @Proceedings{ SPLC:2004, title = {Software Product Line Conference (SPLC)}, year = 2004, key = {SPLC:2004}, booktitle = {Software Product Line Conference (SPLC)}, series = lncs, address = {Boston, USA}, month = {August/September}, publisher = sv } @comment{ ::UM } @Proceedings{ UML:2001, title = {4th International {UML} Conference -- The Unified Modeling Language, Modeling Languages, Concepts, and Tools}, year = 2001, booktitle = {4th International {UML} Conference -- The Unified Modeling Language, Modeling Languages, Concepts, and Tools}, editor = {Martin Gogolla and Cris Kobryn}, volume = 2185, series = lncs, address = {Toronto, Canada}, month = oct, publisher = sv }