Seminar on Specification Languages for Verification

Dates

• You have to hand in your written report until Christmas.
• The talks will take place on Wedenesday, January 25^th and Thursday 26^th, each day starting at 13:00.

Participants

• Functional Reactive Programming (FRP) by Maximilian Krome
• Time Series Database (TSDB) query languages by Philipp Bende

Modules

• CS3702, Bachelor-Seminar Informatik (BachSemInf)
• CS3703, Bachelor-Seminar Medizinische Informatik (BachSemMI)
• CS5480, Seminar Software Systems Engineering (SemSSE)
• CS5840, Englischsprachiges Seminar (SemiEngl)

Subjects

The aim of this seminar is to give an overview on a selection of different specification languages. Available topics include but are not limited to

• Signal Temporal Logic (STL) [1]
• Quantitative Regular Expressions (QRE) [8]
• Lola: Specification Language for Synchronous streams [2]
• Lustre / Scade, Esterel, Signal [3], [4], [5]
• TIMMO TADL2 [6]
• AUTOSAR Timing Extensions (TimeEx) [7]
• Time Series Database (TSDB) query languages
• Functional Reactive Programming (FRP) [11], [12], [13], [14]
• Lucid Synchrone [9] and the new Elm architecture [10]

Please, feel free to propose specific topics that fit the scope of the seminar.

Literature

[1] Oded Maler, Dejan Nickovic: Monitoring properties of analog and mixed-signal circuits. STTT 15(3): 247-268 (2013)
[2] Ben D'Angelo, Sriram Sankaranarayanan, César Sánchez, Will Robinson, Bernd Finkbeiner, Henny B. Sipma, Sandeep Mehrotra, Zohar Manna: LOLA: Runtime Monitoring of Synchronous Systems. TIME 2005: 166-174
[3] Nicolas Halbwachs: A synchronous language at work: the story of Lustre. MEMOCODE 2005: 3-11
[4] Gérard Berry: The foundations of Esterel. Proof, Language, and Interaction 2000: 425-454
[5] Paul Le Guernic, Albert Benveniste, Patricia Bournai, Thierry Gautier: Signal-A data flow-oriented language for signal processing. IEEE Trans. Acoustics, Speech, and Signal Processing 34(2): 362-374 (1986)
[6] Marie-Agnès Peraldi-Frati, Daniel Karlsson, Arne Hamann, Stefan Kuntz, Johan Nordlander: The TIMMO-2-USE project: Time modeling and analysis to use. ERTS2012 International Congres on Embedded Real Time Software and Systems, Feb 2012, Toulouse, France. 2012.
[7] AUTOSAR Development Partnership. Specification of Timing Extensions, Version 1.0.0, Release 4.0.1.
[8] Rajeev Alur, Dana Fisman, Mukund Raghothaman: Regular Programming for Quantitative Properties of Data Streams. ESOP 2016: 15-40
[9] Paul Caspi, Grégoire Hamon, Marc Pouzet: Synchronous Functional Programming: The Lucid Synchrone Experiment. Real-Time Systems: Description and Verification Techniques: Theory and Tools, vol. 1. ISTE 2008
[10] Evan Czaplicki: A Farewell to FRP: Making signals unnecessary with The Elm Architecture. Elm blog. 10 May 2016. http://elm-lang.org/blog/farewell-to-frp
[11] Evan Czaplicki: Elm: Concurrent FRP for Functional GUIs. PhD Thesis. March 2012
[12] Evan Czaplicki, Stephen Chong: Asynchronous functional reactive programming for GUIs. PLDI 2013: 411-422
[13] Zhanyong Wan, Walid Taha, Paul Hudak: Real-Time FRP. ICFP 2001: 146-156
[14] Conal Elliott, Paul Hudak: Functional Reactive Animation. ICFP 1997: 263-273

Your coverage of the your topic shuld not be limited to the literature listed here. See this list as a starting point for your own research instead.

Organization

Participants obtain a dedicated topic from their supervisor and are expected to

• Get acquainted with the individual topic on their own
• Write a technical report: 6 pages IEEE (two-column) format
• Hand in the report (in PDF) 3 weeks before the talk. Hard deadline!
• Give a presentation: 30 min (Bachelor), 45 min (Master), additional 15 min are reserved for discussion
• Hand in complete presentation material (slides as PDF) 1 week before the talk
• Attend all of the presentations

Templates

• The IEEE template for conferences (two-column) must be used for the article.
  • If you use LaTeX you should use the document class IEEEtran with the option conference as shown in the example bare_conf.tex provided in the IEEE template.
  • You should add the document option a4paper to switch from the US paper size letter to european DIN A4.
  • The title of your article should neither contain Specification Languages for Verification nor SpLaV or anything else which is not the title of your article. The current year or term should be omitted as well in the title area.
  • Add your name as author of the article. You may add your email address. Omit any other information in the title area, such as addresses, institution or university names.
  • Start your article with an abstract. Do not give index terms.
  • Avoid page numbers and any other headers or footers.
• For the presentation the ISP LaTeX Beamer template or the universities corporate design can be used.