You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
185 lines
6.3 KiB
185 lines
6.3 KiB
4 years ago
|
<!DOCTYPE html>
|
||
|
|
<html lang="en">
|
||
|
|
<head>
|
||
|
|
<meta charset="utf-8">
|
||
|
|
<title>BaaS: Bisimulation as a Service</title>
|
||
|
|
|
||
|
|
<link rel="stylesheet" media="screen" href="style.css">
|
||
|
|
|
||
|
|
<meta name="viewport" content="width=device-width, initial-scale=1.0">
|
||
|
|
<meta name="author" content="Joshua Moerman">
|
||
|
|
<meta name="description" content="Checking behavioural equivalence was never this easy!">
|
||
|
|
</head>
|
||
|
|
<!--
|
||
|
|
Hi there!
|
||
|
|
|
||
|
|
Great to see you look at the source of this webpage. As you
|
||
|
|
have probably guessed, this is an April fools day joke. Hope
|
||
|
|
you can enjoy :-).
|
||
|
|
|
||
|
|
In case you actually want to compute bisimulations, you can
|
||
|
|
have a look at model checkers such as:
|
||
|
|
- mCRL2: https://www.mcrl2.org
|
||
|
|
- Storm: https://www.stormchecker.org
|
||
|
|
- CADP: https://cadp.inria.fr
|
||
|
|
- UPPAAL: http://www.uppaal.org
|
||
|
|
- Prism: https://www.prismmodelchecker.org
|
||
|
|
Many provide implementations for checking bisimilarity.
|
||
|
|
|
||
|
|
I would like to draw you attention to CoPaR:
|
||
|
|
- https://git8.cs.fau.de/software/copar
|
||
|
|
It is a generic implementation of parition refinement, based
|
||
|
|
on category theory. It implements all the usual bisimulation
|
||
|
|
algorithms (bisimulation, weighted bisimulation, lumping, ...)
|
||
|
|
with a single generic algorithm. In most cases it provides the
|
||
|
|
current best complexity of these algorithms.
|
||
|
|
|
||
|
|
Kind regards,
|
||
|
|
Joshua Moerman
|
||
|
|
-->
|
||
|
|
<body>
|
||
|
|
<div>
|
||
|
|
<section class="intro">
|
||
|
|
<header>
|
||
|
|
<h1>BaaS</h1>
|
||
|
|
<h2>Bisimulation as a Service</h2>
|
||
|
|
</header>
|
||
|
|
|
||
|
|
<div class="summary">
|
||
|
|
<p>Check behavioural equivalence of your models NOW!
|
||
|
|
</div>
|
||
|
|
</section>
|
||
|
|
|
||
|
|
<div class="main">
|
||
|
|
<div class="middle">
|
||
|
|
<h3>What we do as BaaS</h3>
|
||
|
|
<p>We provide an online service for <em>bisimulation checking</em>.
|
||
|
|
Bisimulation is a must in the Industry 4.0 era.
|
||
|
|
Correctness and robustness of your software products are our top priority.
|
||
|
|
With BaaS, we are changing the way you do verification.
|
||
|
|
|
||
|
|
<p>Developers can now check behavioural equivalence with the touch of a button, increasing their productivity.
|
||
|
|
We support many types of bisimulation, including the latest up-to techniques.
|
||
|
|
|
||
|
|
<p>You can register for a monthly subscription which allows you to check many models.
|
||
|
|
We provide a free plan with reduced functionality.
|
||
|
|
</div>
|
||
|
|
|
||
|
|
<div class="solide grid">
|
||
|
|
<div>
|
||
|
|
<img class="cat" src="ginger-cat-746.png"/>
|
||
|
|
</div>
|
||
|
|
|
||
|
|
<div>
|
||
|
|
<h3>What is a bisimulation?</h3>
|
||
|
|
<p>Two systems are <em>bisimilar</em> if they match each other's moves.
|
||
|
|
In this sense, each of the systems cannot be distinguished from the other by an observer.
|
||
|
|
|
||
|
|
<p>A bisimulation relation is a <em>certificate</em> of this equivalence.
|
||
|
|
Our service computes this certificate automatically for you.
|
||
|
|
This makes our service trustworthy and secure, as it does not only return a binary output.
|
||
|
|
|
||
|
|
<p>If your system contains a bug, our service will not be able to produce this certificate.
|
||
|
|
Instead, it will return a counterexample, which can be used to resolve the bug.
|
||
|
|
|
||
|
|
<p>Bisimulations are also used to minimise your state-based systems.
|
||
|
|
This enables model-checkers to prove correctness in terms of temporal logics.
|
||
|
|
</div>
|
||
|
|
|
||
|
|
<div>
|
||
|
|
<h3>Efficient</h3>
|
||
|
|
<p>Our algorithms are state-of-the art, using up-to techniques, making us the most efficient BaaS.
|
||
|
|
These up-to-techniques compress the bisimulation by using algebraic and coalgebraic properties of the system.
|
||
|
|
It allows the bisimulation algorithm to exit early and find bugs more quickly.
|
||
|
|
This is not only good for efficiency and throughput, it also shrinks the size of the certificate.
|
||
|
|
</div>
|
||
|
|
|
||
|
|
<div>
|
||
|
|
<img class="cat" src="ginger-cat-713.png"/>
|
||
|
|
</div>
|
||
|
|
|
||
|
|
<div>
|
||
|
|
<div class="profile">
|
||
|
|
<img class="profile-pic" src="Rob.jpg"><br>
|
||
|
|
Prof. Dr. Rob van Glabbeek.<br>
|
||
|
|
<em>Expert.</em>
|
||
|
|
</div>
|
||
|
|
</div>
|
||
|
|
|
||
|
|
<div>
|
||
|
|
<h3>Testimonial</h3>
|
||
|
|
<p style="font-style:italic">"BaaS is by far the most user-friendly bisimulation checker I have every tried.
|
||
|
|
Small systems, or ones with millions of transitions, Baas gives me the
|
||
|
|
right answers in virtually no time at all. Never again need I
|
||
|
|
experiment with dotted lines on a whiteboard: just pipe it through
|
||
|
|
BaaS and all will be clear!"
|
||
|
|
<p style="text-align:right">- Rob van Glabbeek
|
||
|
|
</div>
|
||
|
|
</div>
|
||
|
|
|
||
|
|
<div class="middle">
|
||
|
|
<h3>BaaS Plans</h3>
|
||
|
|
|
||
|
|
<p>Get in touch to inquire about the pricing.
|
||
|
|
Below is a table of the different features we provide.
|
||
|
|
|
||
|
|
<table>
|
||
|
|
<tr class="rowheader"><th>You get<th>Free<th>Premium BaaS
|
||
|
|
<tr><td>Maximal number of models per month<td>10<td>9000
|
||
|
|
<tr><td>Maximal number of states per model<td>50<td>1000000
|
||
|
|
<tr><td>Maximal number of transitions per model<td>100<td>9000000
|
||
|
|
|
||
|
|
<tr class="rowheader"><th>Features<th><th>
|
||
|
|
<tr><td>Standard (strong) bisimulation<td>✓<td>✓
|
||
|
|
<tr><td>Branching bisimulation<td><td>✓
|
||
|
|
<tr><td>Bisimulation up-to transitive closure and congruence<td><td>✓
|
||
|
|
<tr><td>Bisimulation up-to bisimulation<td><td>✓
|
||
|
|
<tr><td>CEGAR & CEGIS API<td><td>✓
|
||
|
|
<tr><td>O(m log n) algorithms<td><td>✓
|
||
|
|
<tr><td>Big Data Types<!-- Credits to Freek Wiedijk for this joke! --><td><td>✓
|
||
|
|
|
||
|
|
<tr class="rowheader"><th>Models<th><th>
|
||
|
|
<tr><td>Deterministic Automata<td>✓<td>✓
|
||
|
|
<tr><td>Nondeterministic Automata<td><td>✓
|
||
|
|
<tr><td>Weighted Automata<td>✓<td>✓
|
||
|
|
<tr><td>Weighted Tree Automata<td><td>✓
|
||
|
|
<tr><td>Deterministic Register Automata<td><td>✓
|
||
|
|
<tr><td>Markovian Timed Fault Trees<td><td>✓
|
||
|
|
<tr><td>Quantum Software Product Line Systems<td><td>✓
|
||
|
|
<tr><td>Labelled Transition Blockchain Coalgebras<td><td>✓
|
||
|
|
</table>
|
||
|
|
|
||
|
|
<p>Upon request, we can provide <em>divergence-preserving branching bisimilarity</em> for citizens from The Netherlands and France.
|
||
|
|
</div>
|
||
|
|
|
||
|
|
|
||
|
|
<div class="middle">
|
||
|
|
<h3>Team</h3>
|
||
|
|
<p>We're a team of bisimulation technologists and serious entrepreneurs.
|
||
|
|
We work around the clock, to make sure your bisimulations are always ready to go.
|
||
|
|
|
||
|
|
<div class="team">
|
||
|
|
<div class="profile">
|
||
|
|
<img class="profile-pic" src="Joshua.jpg"><br>
|
||
|
|
Joshua Moerman, PhD.<br>
|
||
|
|
Founder, Bisimulation Evangelist.
|
||
|
|
</div>
|
||
|
|
|
||
|
|
<div class="profile">
|
||
|
|
<img class="profile-pic" src="Jurriaan.jpg"><br>
|
||
|
|
Jurriaan Rot, PhD.<br>
|
||
|
|
CEO, CPO, and CTO.
|
||
|
|
</div>
|
||
|
|
</div>
|
||
|
|
</div>
|
||
|
|
|
||
|
|
<footer>
|
||
|
|
Copyright 2020 - BaaS - Bisimulation Online
|
||
|
|
</footer>
|
||
|
|
</div>
|
||
|
|
|
||
|
|
<!-- A bit of a hack. This creates the cats and star! -->
|
||
|
|
<aside></aside>
|
||
|
|
</div>
|
||
|
|
</body>
|
||
|
|
</html>
|