This website serves as an official supplementary portal for our paper, offering open access to implementation artifacts, including source code and experimental datasets. The accompanying README file contains documentation regarding code configuration and the introduction of datasets. Click the button above to download them.
In addition, to compensate for the publication page limitations, we provide supplementary explanations and practical examples here. The website is organized as follows:
Formal Definition: Provides complete formal definitions for TAP smart home integrations modeling and Linear Temporal Logic (LTL), corresponding to the background (Section 2.1 and Section 2.2).
Running Example: Presents more details about the motivating example (Section 2.3), including HAFuzz's input configurations and full execution outputs with interpretations.
RQ1: Accuracy: Demonstrates MEDIC's methodology for automated specification generation from IFTTT rules, forming the technical basis for the evaluation presented in RQ1.
RQ2: Scalability: Shows representative examples in RQ2 of rule-based scenes with different complexity scales.
RQ3: Effectiveness: Showcases complex testing scenarios used in RQ3.
RQ4: Specs Quality: Displays materials featuring the LTL specifications quality assessment used in RQ4 and a sample survey with participant responses.