177 lines
No EOL
6 KiB
HTML
177 lines
No EOL
6 KiB
HTML
<!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>
|
|
|
|
<!--
|
|
Grapje voor 1 april. We moeten nog plaatjes van onszelf toevoegen.
|
|
Misschien ook iets betere plaatjes dan deze katjes...
|
|
|
|
Hier zijn wat goede gratis plaatjes te vinden:
|
|
https://fresh-folk.com/
|
|
https://glazestock.com/
|
|
https://humaaans.com/
|
|
https://icons8.com/ouch
|
|
https://illlustrations.co/
|
|
https://isometric.online/
|
|
https://lukaszadam.com/illustrations
|
|
https://manypixels.co/gallery/
|
|
https://opendoodles.com/
|
|
https://undraw.co/
|
|
https://woobro.design/
|
|
|
|
Misschien moeten we ook een echt lijstje maken voor bisimulatie pakketen.
|
|
Er zijn tools eschikbaar, bijv. in model checkers zoals MCRL2 en Storm,
|
|
maar ook CoPar uit Erlangen is goed om naar te linken.
|
|
Kan ook op een andere pagina, of in een FAQ.
|
|
|
|
Groetjes,
|
|
Joshua
|
|
-->
|
|
|
|
<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>
|
|
<!-- Todo: plaatje -->
|
|
</div>
|
|
|
|
<div>
|
|
<h3>Testimonials</h3>
|
|
<p>Todo.
|
|
Lorem Ipsum is slechts een proeftekst uit het drukkerij- en zetterijwezen. Lorem Ipsum is de standaard proeftekst in deze bedrijfstak sinds de 16e eeuw, toen een onbekende drukker een zethaak met letters nam en ze door elkaar husselde om een font-catalogus te maken. Het heeft niet alleen vijf eeuwen overleefd maar is ook, vrijwel onveranderd, overgenomen in elektronische letterzetting.
|
|
</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>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
|
|
<!-- willen we een email adres? -->
|
|
</footer>
|
|
</div>
|
|
|
|
<!-- A bit of a hack. This creates the cats and star! -->
|
|
<aside></aside>
|
|
</div>
|
|
</body>
|
|
</html> |