OASIcs, Volume 31
FSFMA 2013, July 15-16, 2013, Singapore
Editors: Christine Choppy and Jun Sun
Published in: OASIcs, Volume 31, 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)
1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@Proceedings{choppy_et_al:OASIcs.FSFMA.2013, title = {{OASIcs, Volume 31, FSFMA'13, Complete Volume}}, booktitle = {1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-56-9}, ISSN = {2190-6807}, year = {2013}, volume = {31}, editor = {Choppy, Christine and Sun, Jun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013}, URN = {urn:nbn:de:0030-drops-41281}, doi = {10.4230/OASIcs.FSFMA.2013}, annote = {Keywords: Formal methods} }
Published in: OASIcs, Volume 31, 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)
1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. i-xiii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{choppy_et_al:OASIcs.FSFMA.2013.i, author = {Choppy, Christine and Sun, Jun}, title = {{Frontmatter, Table of Contents, Preface, Workshop Organization}}, booktitle = {1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)}, pages = {i--xiii}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-56-9}, ISSN = {2190-6807}, year = {2013}, volume = {31}, editor = {Choppy, Christine and Sun, Jun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.i}, URN = {urn:nbn:de:0030-drops-40819}, doi = {10.4230/OASIcs.FSFMA.2013.i}, annote = {Keywords: Frontmatter, Table of Contents, Preface, Workshop Organization} }
Published in: OASIcs, Volume 31, 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)
Laurent Fribourg. Control of Switching Systems by Invariance Analysis (Invited Talk). In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, p. 1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{fribourg:OASIcs.FSFMA.2013.1, author = {Fribourg, Laurent}, title = {{Control of Switching Systems by Invariance Analysis}}, booktitle = {1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)}, pages = {1--1}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-56-9}, ISSN = {2190-6807}, year = {2013}, volume = {31}, editor = {Choppy, Christine and Sun, Jun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.1}, URN = {urn:nbn:de:0030-drops-40836}, doi = {10.4230/OASIcs.FSFMA.2013.1}, annote = {Keywords: Control theory, Hybrid systems, Safety, Stability} }
Published in: OASIcs, Volume 31, 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)
Wei-Ngan Chin. Specification, Verification and Inference (Invited Talk). In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, p. 2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{chin:OASIcs.FSFMA.2013.2, author = {Chin, Wei-Ngan}, title = {{Specification, Verification and Inference}}, booktitle = {1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)}, pages = {2--2}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-56-9}, ISSN = {2190-6807}, year = {2013}, volume = {31}, editor = {Choppy, Christine and Sun, Jun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.2}, URN = {urn:nbn:de:0030-drops-40827}, doi = {10.4230/OASIcs.FSFMA.2013.2}, annote = {Keywords: Expressive Specification, Automated Verification, Specification Inference} }
Published in: OASIcs, Volume 31, 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)
Somsak Vanit-Anunchai. Analysis of Two-Layer Protocols: DCCP Simultaneous-Open and Hole Punching Procedures. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 3-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{vanitanunchai:OASIcs.FSFMA.2013.3, author = {Vanit-Anunchai, Somsak}, title = {{Analysis of Two-Layer Protocols: DCCP Simultaneous-Open and Hole Punching Procedures}}, booktitle = {1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)}, pages = {3--17}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-56-9}, ISSN = {2190-6807}, year = {2013}, volume = {31}, editor = {Choppy, Christine and Sun, Jun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.3}, URN = {urn:nbn:de:0030-drops-40846}, doi = {10.4230/OASIcs.FSFMA.2013.3}, annote = {Keywords: Network Address Translators, Coloured Petri Nets, Sweep-line Method, Prioritized Transitions} }
Published in: OASIcs, Volume 31, 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)
Étienne André. Dynamic Clock Elimination in Parametric Timed Automata. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 18-31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{andre:OASIcs.FSFMA.2013.18, author = {Andr\'{e}, \'{E}tienne}, title = {{Dynamic Clock Elimination in Parametric Timed Automata}}, booktitle = {1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)}, pages = {18--31}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-56-9}, ISSN = {2190-6807}, year = {2013}, volume = {31}, editor = {Choppy, Christine and Sun, Jun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.18}, URN = {urn:nbn:de:0030-drops-40855}, doi = {10.4230/OASIcs.FSFMA.2013.18}, annote = {Keywords: Verification, Real-time systems, Parameter synthesis, State space reduction, Inverse Method} }
Published in: OASIcs, Volume 31, 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)
Vladimir-Alexandru Paun, Bruno Monsuez, and Philippe Baufreton. On the Determinism of Multi-core Processors. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 32-46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{paun_et_al:OASIcs.FSFMA.2013.32, author = {Paun, Vladimir-Alexandru and Monsuez, Bruno and Baufreton, Philippe}, title = {{On the Determinism of Multi-core Processors}}, booktitle = {1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)}, pages = {32--46}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-56-9}, ISSN = {2190-6807}, year = {2013}, volume = {31}, editor = {Choppy, Christine and Sun, Jun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.32}, URN = {urn:nbn:de:0030-drops-40869}, doi = {10.4230/OASIcs.FSFMA.2013.32}, annote = {Keywords: multi-core, determinism, hard-real time systems} }
Published in: OASIcs, Volume 31, 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)
César Rodríguez and Stefan Schwoon. An Improved Construction of Petri Net Unfoldings. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 47-52, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{rodriguez_et_al:OASIcs.FSFMA.2013.47, author = {Rodr{\'\i}guez, C\'{e}sar and Schwoon, Stefan}, title = {{An Improved Construction of Petri Net Unfoldings}}, booktitle = {1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)}, pages = {47--52}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-56-9}, ISSN = {2190-6807}, year = {2013}, volume = {31}, editor = {Choppy, Christine and Sun, Jun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.47}, URN = {urn:nbn:de:0030-drops-40875}, doi = {10.4230/OASIcs.FSFMA.2013.47}, annote = {Keywords: Concurrency, Petri nets, partial orders, unfoldings} }
Published in: OASIcs, Volume 31, 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)
Laurent Fribourg, Ulrich Kühne, and Romain Soulat. Constructing Attractors of Nonlinear Dynamical Systems. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 53-60, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{fribourg_et_al:OASIcs.FSFMA.2013.53, author = {Fribourg, Laurent and K\"{u}hne, Ulrich and Soulat, Romain}, title = {{Constructing Attractors of Nonlinear Dynamical Systems}}, booktitle = {1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)}, pages = {53--60}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-56-9}, ISSN = {2190-6807}, year = {2013}, volume = {31}, editor = {Choppy, Christine and Sun, Jun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.53}, URN = {urn:nbn:de:0030-drops-40885}, doi = {10.4230/OASIcs.FSFMA.2013.53}, annote = {Keywords: Control theory, Hybrid Systems, Nonlinear dynamical systems} }
Published in: OASIcs, Volume 31, 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)
Yan Liu. Formal Modelling and Verification of Pervasive Computing Systems. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 61-67, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{liu:OASIcs.FSFMA.2013.61, author = {Liu, Yan}, title = {{Formal Modelling and Verification of Pervasive Computing Systems}}, booktitle = {1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)}, pages = {61--67}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-56-9}, ISSN = {2190-6807}, year = {2013}, volume = {31}, editor = {Choppy, Christine and Sun, Jun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.61}, URN = {urn:nbn:de:0030-drops-40892}, doi = {10.4230/OASIcs.FSFMA.2013.61}, annote = {Keywords: System Analysis, Formal Modelling and Verification, Reliability Analysis} }
Published in: OASIcs, Volume 31, 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)
Jonathan Protzenko. Illustrating the Mezzo programming language. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 68-73, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{protzenko:OASIcs.FSFMA.2013.68, author = {Protzenko, Jonathan}, title = {{Illustrating the Mezzo programming language}}, booktitle = {1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)}, pages = {68--73}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-56-9}, ISSN = {2190-6807}, year = {2013}, volume = {31}, editor = {Choppy, Christine and Sun, Jun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.68}, URN = {urn:nbn:de:0030-drops-40905}, doi = {10.4230/OASIcs.FSFMA.2013.68}, annote = {Keywords: Type system, Language design, ML, Permissions} }
Published in: OASIcs, Volume 31, 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)
Martin Elshuber, Susanne Kandl, and Peter Puschner. Improving System-Level Verification of SystemC Models with SPIN. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 74-79, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{elshuber_et_al:OASIcs.FSFMA.2013.74, author = {Elshuber, Martin and Kandl, Susanne and Puschner, Peter}, title = {{Improving System-Level Verification of SystemC Models with SPIN}}, booktitle = {1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)}, pages = {74--79}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-56-9}, ISSN = {2190-6807}, year = {2013}, volume = {31}, editor = {Choppy, Christine and Sun, Jun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.74}, URN = {urn:nbn:de:0030-drops-40915}, doi = {10.4230/OASIcs.FSFMA.2013.74}, annote = {Keywords: SystemC, SPIN, Promela, System-Level Verification} }
Published in: OASIcs, Volume 31, 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)
Yanti Rusmawati and David Rydeheard. Modelling and Reasoning about Dynamic Networks as Concurrent Systems. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 80-85, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{rusmawati_et_al:OASIcs.FSFMA.2013.80, author = {Rusmawati, Yanti and Rydeheard, David}, title = {{Modelling and Reasoning about Dynamic Networks as Concurrent Systems}}, booktitle = {1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)}, pages = {80--85}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-56-9}, ISSN = {2190-6807}, year = {2013}, volume = {31}, editor = {Choppy, Christine and Sun, Jun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.80}, URN = {urn:nbn:de:0030-drops-40921}, doi = {10.4230/OASIcs.FSFMA.2013.80}, annote = {Keywords: dynamic networks, temporal logic, concurrent systems} }
Published in: OASIcs, Volume 31, 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)
Patrice Carle, Christine Choppy, Romain Kervarc, and Ariane Piel. Safety of Unmanned Aircraft Systems Facing Multiple Breakdowns. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 86-91, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{carle_et_al:OASIcs.FSFMA.2013.86, author = {Carle, Patrice and Choppy, Christine and Kervarc, Romain and Piel, Ariane}, title = {{Safety of Unmanned Aircraft Systems Facing Multiple Breakdowns}}, booktitle = {1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)}, pages = {86--91}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-56-9}, ISSN = {2190-6807}, year = {2013}, volume = {31}, editor = {Choppy, Christine and Sun, Jun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.86}, URN = {urn:nbn:de:0030-drops-40935}, doi = {10.4230/OASIcs.FSFMA.2013.86}, annote = {Keywords: complex event processing, safety, aeronautics, multiple breakdowns, behaviour recognition tool} }
Feedback for Dagstuhl Publishing