arXiv subjects

Tomohiro Oda

Publications and source records attributed to Tomohiro Oda.

7 recordsLinked to original sources

arXiv2026

Trace-Based Execution-Level Observability of VDM-SL Specifications

VDM has been pursuing rigorous verification through mathematical theorem proving and software testing via simulated execution. Animation through an interpreter enables validation of the specification to ensure it meets the required functionality. Step-by-step execution in a debugger also allows the user to follow the internal behavior of operations. In this paper, we propose the recording and utilization of execution traces of assignments, operation calls, and return statements to make the internal behavior of operations persistent and analyzable as state-based models. The data model of events in execution traces, its implementation in ViennaTalk, and its application to visualization will be introduced.

cs.SE↗

arXiv2024

Specification Slicing for VDM-SL

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.

cs.SE↗

arXiv2023

Implementation-First Approach of Developing Formal Semantics of a Simulation Language in VDM-SL

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.

cs.SE↗

arXiv2021

Regional Impacts of COVID-19 on Carbon Dioxide Detected Worldwide from Space

Activity reductions in early 2020 due to the Coronavirus Disease 2019 pandemic led to unprecedented decreases in carbon dioxide (CO2) emissions. Despite their record size, the resulting atmospheric signals are smaller than and obscured by climate variability in atmospheric transport and biospheric fluxes, notably that related to the 2019-2020 Indian Ocean Dipole. Monitoring CO2 anomalies and distinguishing human and climatic causes thus remains a new frontier in Earth system science. We show, for the first time, that the impact of short-term, regional changes in fossil fuel emissions on CO2 concentrations was observable from space. Starting in February and continuing through May, column CO2 over many of the World's largest emitting regions was 0.14 to 0.62 parts per million less than expected in a pandemic-free scenario, consistent with reductions of 3 to 13 percent in annual, global emissions. Current spaceborne technologies are therefore approaching levels of accuracy and precision needed to support climate mitigation strategies with future missions expected to meet those needs.

physics.ao-ph↗

arXiv2021

Proceedings of the 18th International Overture Workshop

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.

cs.SE↗

arXiv2020

Global to local impacts on atmospheric CO2 caused by COVID-19 lockdown

The world-wide lockdown in response to the COVID-19 pandemic in year 2020 led to economic slowdown and large reduction of fossil fuel CO2 emissions, but it is unclear how much it would reduce atmospheric CO2 concentration, and whether it can be observed. We estimated that a 7.9% reduction in emissions for 4 months would result in a 0.25 ppm decrease in the Northern Hemisphere CO2, an increment that is within the capability of current CO2 analyzers, but is a few times smaller than natural CO2 variabilities caused by weather and the biosphere such as El Nino. We used a state-of-the-art atmospheric transport model to simulate CO2, driven by a new daily fossil fuel emissions dataset and hourly biospheric fluxes from a carbon cycle model forced with observed climate variability. Our results show a 0.13 ppm decrease in atmospheric column CO2 anomaly averaged over 50S-50N for the period February-April 2020 relative to a 10-year climatology. A similar decrease was observed by the carbon satellite GOSAT3. Using model sensitivity experiments, we further found that COVID, the biosphere and weather contributed 54%, 23%, and 23% respectively. This seemingly small change stands out as the largest sub-annual anomaly in the last 10 years. Measurements from global ground stations were analyzed. At city scale, on-road CO2 enhancement measured in Beijing shows reduction of 20-30 ppm, consistent with drastically reduced traffic during the lockdown. The ability of our current carbon monitoring systems in detecting the small and short-lasting COVID signal on the background of fossil fuel CO2 accumulated over the last two centuries is encouraging. The COVID-19 pandemic is an unintended experiment whose impact suggests that to keep atmospheric CO2 at a climate-safe level will require sustained effort of similar magnitude and improved accuracy and expanded spatiotemporal coverage of our monitoring systems.

physics.ao-ph↗

arXiv2020

Global Impact of COVID-19 Restrictions on the Atmospheric Concentrations of Nitrogen Dioxide and Ozone

Social-distancing to combat the COVID-19 pandemic has led to widespread reductions in air pollutant emissions. Quantifying these changes requires a business as usual counterfactual that accounts for the synoptic and seasonal variability of air pollutants. We use a machine learning algorithm driven by information from the NASA GEOS-CF model to assess changes in nitrogen dioxide (NO$_{2}$) and ozone (O$_{3}$) at 5,756 observation sites in 46 countries from January through June 2020. Reductions in NO$_{2}$ correlate with timing and intensity of COVID-19 restrictions, ranging from 60% in severely affected cities (e.g., Wuhan, Milan) to little change (e.g., Rio de Janeiro, Taipei). On average, NO$_{2}$ concentrations were 18% lower than business as usual from February 2020 onward. China experienced the earliest and steepest decline, but concentrations since April have mostly recovered and remained within 5% to the business as usual estimate. NO$_{2}$ reductions in Europe and the US have been more gradual with a halting recovery starting in late March. We estimate that the global NO$_{x}$ (NO+NO$_{2}$) emission reduction during the first 6 months of 2020 amounted to 2.9 TgN, equivalent to 5.1% of the annual anthropogenic total. The response of surface O$_{3}$ is complicated by competing influences of non-linear atmospheric chemistry. While surface O$_{3}$ increased by up to 50% in some locations, we find the overall net impact on daily average O$_{3}$ between February - June 2020 to be small. However, our analysis indicates a flattening of the O$_{3}$ diurnal cycle with an increase in night time ozone due to reduced titration and a decrease in daytime ozone, reflecting a reduction in photochemical production. The O$_{3}$ response is dependent on season, time scale, and environment, with declines in surface O$_{3}$ forecasted if NO$_{x}$ emission reductions continue.

physics.ao-ph↗