Haskell-Cafe

Download

haskell-cafe@haskell.org

February 2025

12 participants
12 discussions

[ANN] NASA's Ogma 1.6.0
by Ivan Perez 04 Feb '25

04 Feb '25

Hi everyone! I'm thrilled to announce the release of Ogma 1.6.0! NASA's Ogma is a mission assurance tool that facilitates integrating runtime monitors or runtime verification applications into other systems. Use cases supported by Ogma include producing Robot Operating System (ROS 2) packages [3], NASA Core Flight System (cFS) applications [4], and components for FPrime [1] (the software framework used for the Mars Helicopter). Ogma is also one of the solutions recommended for monitoring in Space ROS applications [2]. Ogma is fully written in Haskell, and leverages existing Haskell work, like the Copilot language [5] (also funded by NASA) and BNFC [6]. For more details, including videos of monitors being generated and flown in simulators, see: https://github.com/nasa/ogma * What's changed This major release includes the following improments: - Update Ogma to be able to extract data from XML files, including standard formats used in MBSE tools. - Provide a new diagram command capable of generating state machine implementations from diagrams. - Make the ROS and F' backend able to use any JSON- or XML files as input, makes the ROS, F', standalone backends capable of using literal Copilot expressions in requirements and state transitions. - Extend Ogma to be able to use external tools to translate requirements, including LLMs. - Make the F' backend able to use templates. - Allow users to provide custom definitions for XML and JSON formats unknown to the tool. - Fixes several other smaller maintenance issues. - Upgrades the README to include instructions for external contributors. This constitutes the single largest release of Ogma in number of new features added, since its first release. For details about the release, see: https://github.com/nasa/ogma/releases/tag/v1.6.0 * Releases Ogma is released as a collection of packages in Hackage. The entry point is https://hackage.haskell.org/package/ogma-cli. * Code The github repo is located at: https://github.com/nasa/ogma. * What's coming The next release is planned for Mar 21st, 2025. We are currently working on a GUI for Ogma that facilitates collecting all mission data relative to the design, diagrams, requirements and deployments, and help users refine designs and requirements, verify them for correctness, generate monitors and full applications, follow live missions, and produce reports. We also want to announce that both Ogma and Copilot can now accept contributions from external users, and we are also keen to see students use them for their school projects, their final projects and theses, and other research. If you are interested in collaborating, please reach out to ivan.perezdominguez(a)nasa.gov. We hope that you are as excited as we are and that our work demonstrates that, with the right support, Haskell can reach farther than we ever thought possible. Happy Haskelling! Ivan [1] https://github.com/nasa/fprime [2] https://space.ros.org/ [3] https://www.ros.org/ [4] https://github.com/nasa/cFS [5] https://github.com/Copilot-Language/copilot [6] https://github.com/BNFC/bnfc

1 0

PhD Position: Verification of Golang using Interactive Theorem Proving (Application Deadline 2025-02-10)
by Achim D. Brucker 04 Feb '25

04 Feb '25

We have an exciting funded opportunity for a PhD on developing "Verification Environment for Distributed Systems Implemented in Go". The main objectives are to define a formal semantics of Go and its CSP-inspired concurrency model in an interactive theorem prover (e.g., Isabelle/HOL) as well as developing a calculus for program verification. This is a unique opportunity to work in the intersection of theory and application and while doing so, contributing to improving the state of the art in software correctness and security. A detailed description of the PhD proposal is available at: * https://www.exeter.ac.uk/v8media/recruitmentsites/documents/A_Verification_… Information about the funding and application process is available at: * https://www.exeter.ac.uk/study/funding/award/?id=5477 Application deadline is the midnight GMT on 10th of February 2025. Please reach out to me, if you have any questions. Best, Achim -- Prof. Achim Brucker | Chair in Cybersecurity & Head of Group | University of Exeter https://www.brucker.ch | https://logicalhacking.com/blog @adbrucker | @logicalhacking

1 0