-
Specification Slicing for VDM-SL
Authors:
Tomohiro Oda,
Han-Myung Chang
Abstract:
The executable specification is one of the powerful tools in lightweight formal software development. VDM-SL allows the explicit and executable definition of operations that reference and update internal state through imperative statements. While the extensive executable subset of VDM-SL enables validation and testing in the specification phase, it also brings difficulties in reading and debugging…
▽ More
The executable specification is one of the powerful tools in lightweight formal software development. VDM-SL allows the explicit and executable definition of operations that reference and update internal state through imperative statements. While the extensive executable subset of VDM-SL enables validation and testing in the specification phase, it also brings difficulties in reading and debugging as in imperative programming. In this paper, we define specification slicing for VDM-SL based on program slicing, a technique used for debugging and maintaining program source code in implementation languages. We then present and discuss its applications. The slicer for VDM-SL is implemented on ViennaTalk and can be used on browsers and debuggers describing the VDM-SL specification.
△ Less
Submitted 4 October, 2024;
originally announced October 2024.
-
Implementation-First Approach of Developing Formal Semantics of a Simulation Language in VDM-SL
Authors:
Tomohiro Oda,
Gaël Dur,
Stéphane Ducasse,
Hugo Daniel Macedo
Abstract:
Formal specification is a basis for rigorous software implementation. VDM-SL is a formal specification language with an extensive executable subset. Successful cases of VDM-family including VDM-SL have shown that producing a well-tested executable specification can reduce the cost of the implementation phase. This paper introduces and discusses the reversed order of specification and implementatio…
▽ More
Formal specification is a basis for rigorous software implementation. VDM-SL is a formal specification language with an extensive executable subset. Successful cases of VDM-family including VDM-SL have shown that producing a well-tested executable specification can reduce the cost of the implementation phase. This paper introduces and discusses the reversed order of specification and implementation. The development of a multi-agent simulation language called \remobidyc is described and examined as a case study of defining a formal specification after initial implementation and reflecting the specification into the implementation code.
△ Less
Submitted 27 March, 2023;
originally announced March 2023.
-
Equilibrium Inverse Reinforcement Learning for Ride-hailing Vehicle Network
Authors:
Takuma Oda
Abstract:
Ubiquitous mobile computing have enabled ride-hailing services to collect vast amounts of behavioral data of riders and drivers and optimize supply and demand matching in real time. While these mobility service providers have some degree of control over the market by assigning vehicles to requests, they need to deal with the uncertainty arising from self-interested driver behavior since workers ar…
▽ More
Ubiquitous mobile computing have enabled ride-hailing services to collect vast amounts of behavioral data of riders and drivers and optimize supply and demand matching in real time. While these mobility service providers have some degree of control over the market by assigning vehicles to requests, they need to deal with the uncertainty arising from self-interested driver behavior since workers are usually free to drive when they are not assigned tasks. In this work, we formulate the problem of passenger-vehicle matching in a sparsely connected graph and proposed an algorithm to derive an equilibrium policy in a multi-agent environment. Our framework combines value iteration methods to estimate the optimal policy given expected state visitation and policy propagation to compute multi-agent state visitation frequencies. Furthermore, we developed a method to learn the driver's reward function transferable to an environment with significantly different dynamics from training data. We evaluated the robustness to changes in spatio-temporal supply-demand distributions and deterioration in data quality using a real-world taxi trajectory dataset; our approach significantly outperforms several baselines in terms of imitation accuracy. The computational time required to obtain an equilibrium policy shared by all vehicles does not depend on the number of agents, and even on the scale of real-world services, it takes only a few seconds on a single CPU.
△ Less
Submitted 12 February, 2021;
originally announced February 2021.
-
Proceedings of the 18th International Overture Workshop
Authors:
John Fitzgerald,
Tomohiro Oda,
Hugo Daniel Macedo
Abstract:
This volume contains the papers presented at the 18th International Overture Workshop, held online on 7th December 2020. This event was the latest in a series of workshops around the Vienna Development Method (VDM), the open-source project Overture, and related tools and formalisms. VDM is one of the longest established formal methods for systems development. A lively community of researchers and…
▽ More
This volume contains the papers presented at the 18th International Overture Workshop, held online on 7th December 2020. This event was the latest in a series of workshops around the Vienna Development Method (VDM), the open-source project Overture, and related tools and formalisms. VDM is one of the longest established formal methods for systems development. A lively community of researchers and practitioners has grown up in academia and industry has grown around the modelling languages (VDM-SL, VDM++, VDM-RT, CML) and tools (VDMTools, Overture, Crescendo, Symphony, the INTO-CPS chain, and ViennaTalk). Together, these provide a platform for work on modelling and analysis technology that includes static and dynamic analysis, test generation, execution support, and model checking. This workshop provided updates on the emerging technology of VDM/Overture, including collaboration infrastructure, collaborative modelling and co-simulation for Cyber-Physical Systems.
△ Less
Submitted 19 January, 2021;
originally announced January 2021.
-
MOVI: A Model-Free Approach to Dynamic Fleet Management
Authors:
Takuma Oda,
Carlee Joe-Wong
Abstract:
Modern vehicle fleets, e.g., for ridesharing platforms and taxi companies, can reduce passengers' waiting times by proactively dispatching vehicles to locations where pickup requests are anticipated in the future. Yet it is unclear how to best do this: optimal dispatching requires optimizing over several sources of uncertainty, including vehicles' travel times to their dispatched locations, as wel…
▽ More
Modern vehicle fleets, e.g., for ridesharing platforms and taxi companies, can reduce passengers' waiting times by proactively dispatching vehicles to locations where pickup requests are anticipated in the future. Yet it is unclear how to best do this: optimal dispatching requires optimizing over several sources of uncertainty, including vehicles' travel times to their dispatched locations, as well as coordinating between vehicles so that they do not attempt to pick up the same passenger. While prior works have developed models for this uncertainty and used them to optimize dispatch policies, in this work we introduce a model-free approach. Specifically, we propose MOVI, a Deep Q-network (DQN)-based framework that directly learns the optimal vehicle dispatch policy. Since DQNs scale poorly with a large number of possible dispatches, we streamline our DQN training and suppose that each individual vehicle independently learns its own optimal policy, ensuring scalability at the cost of less coordination between vehicles. We then formulate a centralized receding-horizon control (RHC) policy to compare with our DQN policies. To compare these policies, we design and build MOVI as a large-scale realistic simulator based on 15 million taxi trip records that simulates policy-agnostic responses to dispatch decisions. We show that the DQN dispatch policy reduces the number of unserviced requests by 76% compared to without dispatch and 20% compared to the RHC approach, emphasizing the benefits of a model-free approach and suggesting that there is limited value to coordinating vehicle actions. This finding may help to explain the success of ridesharing platforms, for which drivers make individual decisions.
△ Less
Submitted 12 April, 2018;
originally announced April 2018.
