arXiv subjects

Margarida Mamede

Publications and source records attributed to Margarida Mamede.

2 recordsLinked to original sources

arXiv2026

Systematic API Testing Through Model Checking and Executable Contracts

Automated black-box testing of APIs typically relies on interface specifications that define available operations and data schemas, but offer limited or no behavioural semantics. This semantic gap amplifies the test-oracle problem and limits the generation of effective, stateful call sequences. We introduce IcePick, a framework that achieves systematic state-space coverage for API testing by leveraging model checking. IcePick uses TLA+ to formally model API state evolution, employs the TLC model checker to exhaustively explore reachable states, and generates test sequences that provably cover the behavioural model. To mitigate state-space explosion and improve sequence extraction, we introduce a coverage-guided breadth-first traversal of the TLC state-space graph. To address oracle limitations beyond HTTP status codes, we propose Glacier, a first-order logic contract language that enriches API specifications with executable semantic contracts, enabling automated behavioural verification during test execution. We evaluate IcePick on EvoMaster Benchmark systems, demonstrating that model-checking-guided exploration achieves complete state coverage and reveals faults in multi-operation interactions. We also analyse scalability to characterise practical limits and applicability requirements. Overall, IcePick provides reproducible test suites with strong coverage guarantees for critical API-based systems.

cs.SE↗

arXiv2016

Relieving Core Routers from Dynamic Routing with off-the-shelf Equipment and Protocols

To answer traffic engineering goals, current backbone networks use expensive and sophisticated equipments, that run distributed algorithms to imple- ment dynamic multi-path routing (e.g., MPLS tunnels and dynamic trunk rerout- ing). We think that the same goals can be fulfilled using a simpler approach, where the core of the backbone only implements many a priori computed paths, and most adaptation to traffic engineering goals only takes place at the edge of the network. In the vein of Software Defined Networking, edge adaptation should be driven by a logically centralized controller that leverages the available paths to adapt traffic load balancing to the current demands and network status. In this article we present two algorithms to help building this vision. The first one selects sets of paths able to support future load balancing needs and adaptation to network faults. As the total number of required paths is very important, and their continuous availability requires many FIB entries in core routers, we also present a second algorithm that aggregates these paths in a reduced number of trees. This second algorithm achieves better results than previously proposed algorithms for path aggregation. To conclude, we show that off-the-shelf equipment supporting simple protocols may be used to implement routing with these trees, what shows that simplicity in the core can be achieved by using only trivially available proto- cols and their most common and unsophisticated implementation

cs.NI↗