search

hallba / BioModelAnalyzer

BioModelAnalyzer is a user-friendly tool for constructing biological models and verifying them
Other
6 stars 2 forks source link

readme

BMA Build Build status Tests

The BioModelAnalyzer is a tool that allows biologists to easily and quickly build complex models of biological behaviour, and to analyse them using techniques derived from the field of formal verification. Its backend is written in F#, and its graphical frontend is an HTML5 application. It uses the SMT solver Z3.

This consists of

The goal of the project is to provide access to biologists to powerful, newly developed algorithms without requiring expertise in the underlying computer science. This is achieved by bespoke user interfaces and novel methods of interaction. The aims of the project are to increase the range of modelling and analysis approaches made available through the tool, and to extend the interface to increase the ease of user adoption.

The user interface is considered as production quality, whilst all other tools are regarded as prototypes in different stages of readiness.

The three goals on the project roadmap are to add more advanced library and comparison functions to the user interface, to expand the range of concurrency types available in the tool, and to add support for alternative model formats. This are intended to be addressed over the next 2-3 years.

Contributions are welcome! Bugs or feature requests should be reported to the team, whilst code contributions should follow the instructions in CONTRIBUTING.md.

Contents

Structure of repository

Powershell scripts in the root of repository (PowerShell 5.0 or above is required):

/sln - Visual Studio solutions:

/ChatBot - A chat bot intended for user education in linear temporal logic.

/src - Visual Studio projects. A project can be shared between multiple solutions.

/docs - Project documentation.

/ext/FParsec contains third party source code of FParsec, a parser combinator library for F#. BioModelAnalyzer depends on this library.

/ext/CUDD contains third party source code of CUDD, a binary decision diagram library for C++. Some functionality of BioModelAnalyzer depends on this library.

/Models contains biological models that can be imported from the BioModelAnalyzer application.

Build and test

The rest of building, testing, and deployment processes heavily rely on this first step having been performed. The script downloads paket and runs it in order to fetch the external dependencies. Also the script creates local files /src/ApiServer/unity.azure-appservice.config and /src/ApiService/ServiceConfiguration.Cloud.cscfg with default Azure deployment configurations. These files are configured to be ignored by git and will not be committed to the repository, thus they may contain Azure Storage Account connection strings.

Build requirements

  1. Visual Studio 2015/2017. If you don't have Visual Studio 2015/2017, you can install the free Visual Studio 2015/2017 Community. Currently the build process relies on tools that come with Visual Studio 2015/2017 such as Microsoft .NET Framework 4.5, Microsoft Build Tools, Web Applications Build Targets, Visual F# Tools, TypeScript compiler and Visual C++.

  2. Visual F# Tools 4.0. The Visual F# Tools are installed automatically when you first create or open an F# project in Visual Studio. If you run the build script without using Visual Studio IDE you can install it directly as a separate download.

  3. TypeScript 1.8. Certain versions of Visual Studio can install different versions of TypeScript by default, so you need to install TypeScript 1.8 from Microsoft web site.

How to Build

After the repository is prepared using the script PrepareRepository.ps1, you can build the solutions using Visual Studio or msbuild.

Also there are helpful build-related scripts located in the root of repository:

How to Test and Validate

Regression tests

Solution /sln/bmaclient contains following test projects:

Deployment tests

Solution /sln/bmaclient contains test project WebApiTests that sends requests represented as files in /src/BmaTests.Common/Simulation, /src/BmaTests.Common/Analysis, /src/BmaTests.Common/CounterExamples and /src/BmaTests.Common/LTLQueries to the deployed ApiServer and checks the responses. Server url is configured in the WebApiTests.fs.

This allows to check if the deployed server correctly performs operations.

End-to-end tests

End-to-end tests for bma.client web application are located in /src/CodedUITests. They are based on Protractor framework.

How to run tests in Visual Studio

Note that running tests for x64 requires setting default processor architecture for tests to x64. In Visual Studio 2015/2017, use menu Test/Test Settings/Default Processor Architecture.

Run and deploy

Here we describe how to run and deploy BioModelAnalyzer which consists of two web applications: ApiServer and bma.client.

Please see /docs/BMA Deployment Overview.pptx for details about BioModelAnalyzer architecture.

In the followings guidelines we will use Visual Studio 2015/2017. The solution that produces the web applications is located in /sln/bmaclient. Please make sure that you have run the powershell script ./PrepareRepository.ps1 as described in the Build and test section to prepare the repository.

Local run using IIS Express

This deployment is useful when developing the applications. It allows easily debugging the applications using Visual Studio.

1. Choose the platform for the solution.

Use Visual Studio interface to select the solution platform, either x86 or x64.

In Visual Studio menu, click Tools/Options/Projects and Solutions/Web Projects and check or uncheck the option Use the 64 bit version of IIS Express for web sites and projects.

2. Update activity and failure logs configurations for APIServer.

Open ApiServer/Web.config and uncomment the unity configuration source unity.web.config to write the activity and failure logs to local CSV files or unity.trace-loggers.config to write logs to System.Diagnostics.TraceSource:

<unity configSource="unity.web.config"/>

OR

<unity configSource="unity.trace-loggers.config"/>

Make sure that only one <unity /> configuration is uncommented. See more details in the Activity and failure logs section of this document.

3. Choose the IIS Express to be used as server.

Open Properties for the project ApiServer and go to section Web. In the group Servers, choose IIS Express and check the Project Url text which contains url of the ApiServer application. By default, it is http://localhost:8223.

4. Set ApiServer as start-up project.

In the context menu for the ApiServer, click on the Set as StartUp Project command. The project name should become bold in the Solution Explorer.

5. Run ApiServer.

In menu Debug click either Start Debugging or Start Without Debugging. After the project is built and run, a browser window should open with the project url. Most browsers normally show HTTP Error 403.14 - Forbidden because the root of the site is forbidden and no default document is configured.

Now the ApiServer is available at http://localhost:8223. Next we will run bma.client web site which allows using the BioModelAnalyzer HTML application to build and analyze models.

6. Update BackEndUrl for the bma.client application.

We should specify url of the ApiServer for the bma.client to send user requests, such as model analysis and simulation. Edit the bma.client/Web.config so the <appSettings> contains key BackEndUrl:

  <appSettings>   
    <add key="BackEndUrl" value="http://localhost:8223" />    
  </appSettings>

Note that other two app settings, LiveAppId and RedirectUrl, are for integration with OneDrive which is unavailable for local host and thus can be ignored here.

7. Choose the IIS Express to be used as server for bma.client.

Open Properties for the project bma.client and go to section Web. In the group Servers, choose IIS Express.

8. Set bma.client as start-up project.

In the context menu for the bma.client, click on the Set as StartUp Project command. The project name should become bold in the Solution Explorer.

9. Run bma.client.

After the project is built and run, a browser window should open with the project url. Normally you see the start-up screen with logo and Launch Tool button. Also you can click Help link at the top and load one of the examples.

You can run WebApiTests for the deployed ApiServer to check whether it works correctly; see section Deployment tests in this document.

Self-hosting application using OWIN

BMA can be hosted using OWIN. This is convenient for development and debugging, and it allows to use BMA standalone.

For those purposes the repository contains bma.selfhost application. It hosts BMA using OWIN making both API and UI available at http://localhost:8224/ and it stores logs in local files (see Activity and failure logs for details).

You can start it either by running run.ps1 powershell script located in the root of repository (in which case your system's architecture will be used) or you can find it within /sln/bmaclient solution. The script will also open a browser window with BMA UI for you as soon as it is available. If you choose not to use the script and to run the application directly instead, then, in order to access BMA UI you'll have to open http://localhost:8224/ in your browser.

You can run WebApiTests with server url set to http://localhost:8224/ to check if it works correctly; see Deployment tests for details.

Deployment in Azure App Services

This deployment allows to publish BMA web application for public use. Azure allows scaling the applications and distributes demand between multiple copies of an application.

Quick deployment using included script

Included powershell script DeployAzure.ps1 quickly deploys BMA using a free tier App Service plan to host API and UI and a locally-redundant storage account for logging. Simply run in powershell console

.\DeployAzure.ps1 <name>

and log into Azure when prompted to deploy UI to https://\<name>.azurewebsites.net and API to https://\<name>api.azurewebsites.net.

It's possible to customize the names of deployed resources using script arguments. Run

Get-Help .\DeployAzure.ps1 -detailed

for details.

Custom deployment using Visual Studio

1. Update activity and failure logs configurations for ApiServer.

<unity configSource="unity.azure-appservice.config"/>

Make sure that only one <unity /> configuration is uncommented.

2. Publish ApiServer

The first time you publish the application you need to create an Azure App Service, choose a resource group and a service plan. All these settings will be saved as a publish profile file in the folder /src/ApiServer/Properties/PublishProfiles, so next deployments will be very simple.

  1. In Visual Studio, in the context menu for the ApiServer project, click Publish...
  2. Select Microsoft Azure App Service as a publish target.
  3. In the App Service window, you should either create new app service (if you do this first time), or choose previously created app service. For the first time, click New.
  4. Click Change Type and choose API App.
  5. Enter API App Name, for example, BioModelAnalyzerAPI.
  6. Choose your Azure Subscription.
  7. Choose existing or create new Resource Group. In Azure, related resources such as app services, storage accounts and service plans are logically grouped to be managed as a single entity. So it makes sense to create a Resource Group for BMA.
  8. Choose existing or create new App Service Plan. The plan determines power and cost of the services. If you choose free plan, you cannot use x64 platform.
  9. Click Create and wait until all deployment steps completed.
  10. In the Publish window, make sure that Publish method is Web Deploy. Check site name and click Next.
  11. Select configuration, e.g. Release - x86. If you need x64, please read section Choosing the platform architecture (32-bit or 64-bit) of this document, because there are certain requirements for service plan.
  12. Click Next, then Publish. Visual Studio will start building the solution for the selected configuration. If build succeeds, the application will be deployed in Azure and Visual Studio will open a browser for the application's url, e.g. http://biomodelanalyzerapi.azurewebsites.net/.

Since the publish profile exists, deployment update is very simple:

  1. In Visual Studio, in the context menu for the ApiServer project, click Publish....
  2. In the Publish window, click Publish.
  3. If the password wasn't cached on your machine, Visual Studio will ask your for the password. To find the password,
    1. Open https://portal.azure.com.
    2. Click App Services.
    3. Click the published Api App, for example, BioModelAnalyzerAPI.
    4. Click ...More button and then Get publish profile.
    5. In the downloaded file, find userPWD and use it as the password.

In the Publish window it is possible to click Profile button and create another publish profile. You can then choose between existing publish profiles.

So far the API App is published. Next we should publish web application bma.client.

3. Setup OneDrive access for bma.client

If you want to enable OneDrive functionality (allow users to use their OneDrive as model storage), you have to register your deployment at OneDrive and modify bma.client's Web.config file accordingly. To do so,

<configuration>
  <appSettings>
    <add key="LiveAppId" value="..." /> <!--Live app ID goes here. Get it from the onedrive reg site-->
    <add key="RedirectUrl" value="https://<domain>/html/callback.html" />
    ...
  </appSettings>
  ...
</configuration>

There is no need to register new application if you just want to move to a new domain. You only need to update the redirect URI (both in the settings of your OneDrive App and the Web.config file).

4. Update BackEndUrl for the bma.client application

Edit Web.config to provide url of the published ApiServer. BackEndUrl should be URI of the ApiServer, e.g. http://biomodelanalyzerapi.azurewebsites.net/. 

<configuration>
  <appSettings>    
    <add key="BackEndUrl" value="--- url of the ApiServer ---" />
    ...
  </appSettings>
  ...
</configuration>

5. Update application version

If you publish new version of BioModelAnalyzer application, you need to increase its version number. To do that, edit bma.client/version.txt.

6. Publish bma.client

The first time you publish the application you need to create an Azure App Service, choose a resource group and a service plan. All these settings will be saved as a publish profile file in the folder /src/bma.client/Properties/PublishProfiles, so next deployments will be very simple.

  1. In Visual Studio, in the context menu for the bma.client project, click Publish...
  2. Select Microsoft Azure App Service as a publish target.
  3. In the App Service window, you should either create new app service (if you do this first time), or choose previously created app service. For the first time, click New.
  4. Click Change Type and choose Web App.
  5. Enter Web App Name, for example, BioModelAnalyzerClient.
  6. Choose same Azure Subscription as for ApiServer.
  7. Choose the Resource Group you previously selected for the ApiServer.
  8. Choose the App Service Plan you previously selected for the ApiServer.
  9. Click Create and wait until all deployment steps completed.
  10. In the Publish window, make sure that Publish method is Web Deploy. Check site name and click Next.
  11. Select configuration. It is not significant for this application, so you can choose Release - x86.
  12. Click Next, then Publish. Visual Studio will start building the solution for the selected configuration. If build succeeds, the application will be deployed in Azure and Visual Studio will open a browser for the application's url. If you enabled OneDrive, you must use https, e.g. http://biomodelanalyzerclient.azurewebsites.net/, otherwise OneDrive will fails.

Since the publish profile exists, deployment update is very simple:

  1. In Visual Studio, in the context menu for the bma.client project, click Publish...
  2. In the Publish window, click Publish.
  3. If the password wasn't cached on your machine, Visual Studio will ask your for the password. To find the password,
    1. Open https://portal.azure.com.
    2. Click App Services.
    3. Click the published Web App, for example, BioModelAnalyzerClient.
    4. Click ...More button and then Get publish profile.
    5. In the downloaded file, find userPWD and use it as the password.

In the Publish window it is possible to click Profile button and create another publish profile. You can then choose between existing publish profiles.

After the project is deployed, a browser window should open with the project url. Normally you see the start-up screen with logo and Launch Tool button. Also you can click Help link at the top and load one of the examples.

You can run WebApiTests for the deployed ApiServer to check whether it works correctly; see section Deployment tests in this document.

Scale up and Scale out

In Azure, a scale up operation allows to choose bigger or smaller server depending on your needs. A scale out operation creates multiple copies of a web application and adds a load balancer to distribute demand between them. The article Scale up an app in Azure shows how to scale an application in Azure App Service.

Choosing the platform architecture (32-bit or 64-bit)

In Visual Studio, change current platform for the solution to either x86 or x64. Note that applications built for x86 work on x64 platform, but not vice versa. If you deploy it then, this selection must correspond to settings of web hosting or Azure application settings, otherwise you will get Internal Server Error when trying to access the services. This error is caused by BadImageFormatException thrown by the web application.

In Azure App Service, the 64-bit platform can be enabled in Basic plans and higher. Open Azure Portal, find and click the deployed web application and then open its Application Settings and check Platform.

To run the applications using IIS Express in Visual Studio, open Tools/Options/Projects and Solutions/Web Projects and check or uncheck the option Use the 64 bit version of IIS Express for web sites and projects.

Activity and failure logs

ApiServer exposes /api/activitylog endpoint to gather user activity statistics from BMA client. Browser sends a message to this endpoint when a user closes the BMA page.

Also, ApiServer stores information about failures during simulations and analysis performed for BMA client. It saves the failed request and error message so it is possible to reproduce the error case.

Location and format of logs is determined by the Unity config files used by ApiServer and depend on deployment type. See Unity configuration file samples in following sections.

<unity xmlns="http://schemas.microsoft.com/practices/2010/unity">
  <container>
    <register type="BMAWebApi.IFailureLogger, BMAWebApi"
              mapTo="BMAWebApi.FailureFileLogger, BMAWebApi">
      <constructor>
        <param name="dir"
               value="Failures" />
        <param name="tryServerPath"
               value="True" />
      </constructor>
    </register>

    <register type="BMAWebApi.IActivityLogger, BMAWebApi"
              mapTo="BMAWebApi.ActivityFileLogger, BMAWebApi">
      <constructor>
        <param name="dir"
               value="ActivityLog" />
        <param name="tryServerPath"
               value="True" />
      </constructor>
    </register>
  </container>
</unity>
<unity xmlns="http://schemas.microsoft.com/practices/2010/unity">
  <container>
    <register type="BMAWebApi.IFailureLogger, BMAWebApi"
              mapTo="BMAWebApi.FailureTraceLogger, BMAWebApi">
      <constructor>
        <param name="traceSourceName"
               value="BioModelAnalyzer" />
        <param name="eventId"
               value="1" />
      </constructor>
    </register>

    <register type="BMAWebApi.IActivityLogger, BMAWebApi"
              mapTo="BMAWebApi.ActivityTraceLogger, BMAWebApi">
      <constructor>
        <param name="traceSourceName"
               value="BioModelAnalyzer" />
        <param name="eventId"
               value="2" />
      </constructor>
    </register>
  </container>
</unity>

How to release

Here we describe how to release new version of the BioModelAnalyzer application which is represented by the solution /sln/bmaclient.

  1. Update /src/bma.client/version.txt so it contains new version number for the BioModelAnalyzer release.
  2. Add new section to /RELEASE_NOTES.md which describes the releasing version and contains summary, new features and bug fixes lists.
  3. Build the bmaclient solution in the Release configuration both for x86 and x64 platforms. See How to Build.
  4. Run regression tests for both platforms. All tests must pass. See How to Test and Validate.
  5. Run BioModelAnalyzer locally or make test deployment then run deployment and end-to-end tests. See Run and deploy.
  6. Create a GitHub release. See Creating Releases.
  7. Deploy new version of BioModelAnalyzer to a production server.
  8. Test the production deployment using deployment tests.