Verificação paralela de sistemas dinâmicos com configurações ricas

Master thesis English OPEN
Pessoa, Eduardo José Dias;
(2016)
  • Subject: Electrum | Alloy | Model-Checking | Configurações ricas | TLA | Verificação paralela | Formal specification language | Parallel verification | Linguagem de especificação formal | Sistemas dinâmicos | Verificação de modelos | :Engenharia Eletrotécnica, Eletrónica e Informática [Engenharia e Tecnologia] | Rich configurations | Dynamic systems

Dissertação de mestrado em Engenharia Informática (área de especialização em Informática) Model checking is a technique used to automatically verify a model which represents the specification of some system. To ensure the correctness of the system the verification... View more
  • References (12)
    12 references, page 1 of 2

    4.1 TimeConstraints relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 4.2 TimeConstraints formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 5.1 Original bounds following Alloy . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 5.2 Solution returned by Kodkod in Alloy . . . . . . . . . . . . . . . . . . . . . . . . . 75 5.3 Original bounds following Electrum . . . . . . . . . . . . . . . . . . . . . . . . . . 76 5.4 Solution returned by Kodkod in Electrum . . . . . . . . . . . . . . . . . . . . . . . 76 6.1 First configuration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 6.2 Second configuration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 6.3 The bounds of an integrated problem Pi . . . . . . . . . . . . . . . . . . . . . . . . 85 Armin Biere. Lingeling, plingeling, picosat and precosat at sat race 2010. FMV Report Series Technical Report, 10(1), 2010.

    Armin Biere, Alessandro Cimatti, Edmund M Clarke, Ofer Strichman, and Yunshan Zhu. Bounded model checking. Advances in computers, 58:117-148, 2003.

    Jasmin Christian Blanchette and Tobias Nipkow. Nitpick: A counterexample generator for higherorder logic based on a relational model finder. In Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pages 131- 146, 2010. doi: 10.1007/978-3-642-14052-5 11. URL http://dx.doi.org/10.1007/ 978-3-642-14052-5_11.

    Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta. The nuxmv symbolic model checker. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, pages 334-342, 2014. doi: 10.1007/978-3-319-08867-9 22. URL http://dx.doi.org/10.1007/ 978-3-319-08867-9_22.

    Alcino Cunha. Bounded model checking of temporal formulas with alloy. In Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Toulouse, France, June 2- 6, 2014. Proceedings, pages 303-308, 2014. doi: 10.1007/978-3-662-43652-3 29. URL http: //dx.doi.org/10.1007/978-3-662-43652-3_29.

    Greg Dennis, Felix Sheng-Ho Chang, and Daniel Jackson. Modular verification of code with SAT. In Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2006, Portland, Maine, USA, July 17-20, 2006, pages 109-120, 2006. doi: 10.1145/1146238. 1146251. URL http://doi.acm.org/10.1145/1146238.1146251.

    Niklas Ee´n and Niklas So¨rensson. An extensible SAT-solver. In Theory and Applications of Satisfiability Testing, 6th International Conference, SATModular verification of code with 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers, pages 502- 518, 2003. doi: 10.1007/978-3-540-24605-3 37. URL http://dx.doi.org/10.1007/ 978-3-540-24605-3_37.

    Marcelo F. Frias, Juan P. Galeotti, Carlos Lo´pez Pombo, and Nazareno Aguirre. Dynalloy: upgrading Alloy with actions. In 27th International Conference on Software Engineering (ICSE 2005), 15-21 May 2005, St. Louis, Missouri, USA, pages 442-451, 2005. doi: 10.1145/1062455.1062535. URL http://doi.acm.org/10.1145/1062455.1062535.

    Juan P. Galeotti, Nicola´s Rosner, Carlos Lo´pez Pombo, and Marcelo F. Frias. Analysis of invariants for efficient bounded verification. In Proceedings of the Nineteenth International Symposium on Software Testing and Analysis, ISSTA 2010, Trento, Italy, July 12-16, 2010, pages 25-36, 2010. doi: 10.1145/1831708.1831712. URL http://doi.acm.org/10.1145/1831708.1831712.

    Lu´ıs Gil, Paulo F. Flores, and Lu´ıs Miguel Silveira. PMSat: a parallel version of MiniSAT. JSAT, 6 (1-3):71-98, 2009. URL http://jsat.ewi.tudelft.nl/content/volume6/JSAT6_ 5_Gil.pdf.

  • Similar Research Results (2)
  • Metrics
Share - Bookmark