Advertisement
Published in:
2020 | OriginalPaper | Chapter
Formal Specification and Model Checking of a Ride-sharing System in Maude
Authors : Eiichi Muramoto, Kazuhiro Ogata, Yoichi Shinoda
Published in: Structured Object-Oriented Formal Language and Method
Publisher: Springer International Publishing
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Abstract
We report on a case study in which we have formally specified a ride-sharing system in Maude, a rewriting logic-based specification/programming language and model checked that the system enjoys desired liveness as well as safety properties with the Maude LTL model checker. In our approach to formal specification of the system, a map, a collection of cars and a collection of persons are treated as parameters. Thus, it suffices to write one formal systems specification from which the specification instance is generated for each fixed map, each fixed collection of cars and each fixed collection of persons. We often need fairness assumptions to model check liveness properties, which makes model checking performance slower or even infeasible. The case study also demonstrates that such a situation can be alleviated by a divide & conquer approach to liveness model checking under fairness.