Check my GitHub page!
Joint work with Fabricio Chalub.
Maude MSOS Tool (MMT) is an execution environment for Modular Structural Operational Semantics (MSOS) specifications that brings the power of analysis available in the Maude system to MSOS specifications.
MSOS, developed by Mosses, is a modular variant of Plotkin’s SOS. Like SOS, MSOS is a framework suitable for the specification of a wide range of computational formalisms, including programming language semantics, and concurrent systems. Unlike SOS, MSOS has the advantage of being able to specify completely modular specifications, an advantage when considering the engineering decisions that one must face when designing complex or “exploratory” — when new features to be implemented are not known in advance — specification projects. As an example: consider an SOS specification of a functional language fragment with environments; if imperative features must be added later to the language, therefore requesting a store component to be considered, all rules written for the functional language fragment would have to be retracted and replaced by new rules that also involve the store component. MSOS makes this unnecessary by structuring the labels as records of semantic components, such as the environment and the store, and abstracting from the rules the fact that new components may be added in future extensions.
MMT is formally designed, which means that it is an implementation of a semantics-preserving mapping from MSOS to rewriting logic. MMT supports a specification language, designed by Mosses and Chalub, called MSDF, the Modular SOS Specification Formalism, which is a language that combines an extended-BNF notation for the definition of abstract grammar and a textual representation for MSOS transitions that captures mathematical notation commonly used in papers and textbooks, making the language itself based on well known “user-friendly” notations available on the literature.
Joint work with Cássio Santos.
ECore Consistency Checker (ECC) is a tool designed to identify consistency errors in class and object diagrams. Implementing state-of-the-art research on formal model verification by mapping ECore diagrams to logical theories in Description Logics (DL), ECC aims at detecting software errors in stages that precedes coding in the development process.
Ecore Consistency Checker is Open Source and licensed under the GNU General Public License Version 3. (Copyright (c) 2015, Santos, C. & Braga, C.) ECC uses other free libraries:
- OWL API (licensed under LGPL, Version 3.0)
- DL-Learner (licensed under GPL, Version 3.0)
- HermiT (licensed under LGPL, Version 3.0)
Joint work with Hugo Farias.
Massive open online courses (MOOC) allows for distributed long-distance learning for extremely large student enrollment. Nowadays most universities throughout the world have their courses online. Web portals such as Coursera or edX join together courses from many of them. Even though there are many platforms to support the development of MOOC, such as Moodle or XBlock, it does not seem to be the case that there are many languages to help course descriptions. Moreover, we would like to allow the description of different paths to teach and learn a given subject. We propose Learn, a declarative language for course descriptions and the Learn Maude Toolkit (LMT), an execution environment for Learn descriptions.