search

mbeddr / mbeddr.formal

FASTEN: FormAl SpecificaTion ENvironment - a set of DSLs to experiment with rigorous systems and safety engineering.
https://sites.google.com/site/fastenroot/home
Apache License 2.0
23 stars 14 forks source link
architecture contract-based-design gsn interface-specification jetbrains-mps mbeddr nusmv prism requirements-specification safety-assurance spin stpa z3

readme

FASTEN

Homepage

Community

Versions

Building (from command line)

For building FASTEN we have Gradle-based scripts which automatically manage all needed dependencies including MPS itself and build the languages.

  1. configure the needed variables in gradle.properties:
    • copy the gradle.properties.example as gradle.properties and replace "<...>" with your paths, github-username and a token with rights to access github-packages
      • in Windows please note that the paths should use slash instead of back-slash, and they must NOT contain any space character (' ') - e.g. 
        mpsHomeDir=C:/work/MPS_2023.2
mbeddr.formal.home=C:/work/mbeddr.formal
gpr.user=<a github user name>
gpr.token=<token for package access>
      • in Unix-based systems we have the "unix paths" (nothing changes)
  2. run gradlew.bat- this starts the default task which downloads dependencies and builds FASTEN languages
    • if you want to build the standalone distribution (RCP) run gradlew.bat build_fasten_safety_distribution
      • you can find the zip in the directory "build\artifacts\com.mbeddr.formal.safetyDistribution"

Building (from MPS)

  1. download and install MPS 2023.2
  2. run gradlew.bat setup. You can skip this step if you have built the project with Gradle already.
  3. start MPS
  4. in 'Settings->Appearance & Behavior->Path Variables', set the path variable mbeddr.formal.home to point to the directory which contains the cloned 'mbeddr.formal' repository.
  5. FASTEN sources are organized in several MPS projects. To build FASTEN, each of these projects need to be built. Please open and build the projects in the following order:
    1. code\languages\com.mpsbasics
    2. code\languages\com.mbeddr.formal.nusmv
      1. after this build is successful, you should be able to open the code\tutorial project (contains only SMV-based DSLs)
    3. code\languages\com.mbeddr.formal.req
    4. code\languages\com.mbeddr.formal.spin
    5. code\languages\com.mbeddr.formal.safety

After the above steps you should be able to open code\tutorial-safety project - it contains the DSLs related to safety.