Advances and standards in Internet of Things (IoT) have simplified the realization building automation. However, non-expert IoT users still lack tools that can help them to ensure underlying control system correctness: user-programmable logics match user intention. In fact, necessary know-how domain experts. This paper presents our experience running a automation service based on Salus framework. Complementing efforts simply verify correctness, takes novel steps tackle practical challenges...

A large number of functionality-rich and easily accessible applications have become popular among various virtual personal assistant (VPA) services such as Amazon Alexa. VPA (or apps for short) are accompanied by a privacy policy document that informs users their data handling practices. These documents usually lengthy complex to comprehend, developers may intentionally or unintentionally fail comply with them. In this work, we conduct the first systematic study on compliance issue apps. We...

Many Cyber-Physical Systems (CPS) are highly nondeterministic. This often makes it impractical to model and predict the complete system behavior. To address this problem, we propose that instead of offline modeling verification, many CPS systems should be modeled verified online, shall focus on system's time-bounded behavior in short-run future , which is more describable predictable. Meanwhile, as generated/updated verification has fast. It meaningless tell an online unsafe when already...

Hybrid automata are well studied formal models for hybrid systems with both discrete and continuous state changes. However, the analysis of is quite difficult. Even simple class linear automata, reachability problem undecidable. In author's previous work, we proposed a programming based approach to check one path at time while length size automaton being checked can be large enough handle problems practical interest. Based on this approach, in paper present prototype tool BACH perform...

Hybrid systems model checking is a great success in guaranteeing the safety of computerized control cyber-physical (CPS). However, when applying hybrid to Medical Device Plug-and-Play (MDPnP) CPS, we encounter two challenges due complexity human body: 1) there are no good offline differential equation-based models for many body parameters; 2) can result variables, complicating system model. In an attempt address challenges, propose alter traditional approach time-unbounded (i.e., infinite...

Symbolic execution is a widely-used program analysis technique. It collects and solves path conditions to guide the traversing. However, due limitation of current constraint solvers, it difficult apply symbolic on programs with complex conditions, like nonlinear constraints function calls. In this paper, we propose new tool MLB handle such problem. Instead relying classical solving, in MLB, feasibility problems are transformed into optimization problems, by minimizing some dissatisfaction...

Formal program specifications play a crucial role in various stages of software development. However, manually crafting formal is rather difficult, making the job time-consuming and labor-intensive. It even more challenging to write that correctly comprehensively describe semantics complex programs. To reduce burden on developers, automated specification generation methods have emerged. existing usually rely predefined templates or grammar, them struggle accurately behavior functionality...

The rise of code pre-trained models has significantly enhanced various coding tasks, such as completion, and tools like GitHub Copilot. However, the substantial size these models, especially large poses a significant challenge when it comes to fine-tuning them for specific downstream tasks. As an alternative approach, retrieval-based methods have emerged promising solution, augmenting model predictions without need fine-tuning. Despite their potential, is that designs often rely on...

Recent advances and industry standards in Internet of Things (IoT) have accelerated the real-world adoption connected devices. To manage this hybrid system digital real-time devices analog environments, has pushed several popular home automation IoT (HA-IoT) frameworks, such as If-This-Then-That (IFTTT), Apple HomeKit, Google Brillo. Typically, users author device interactions by specifying triggering sensor event triggered command. In seemingly simple software system, two dominant factors...

With many trigger-action platforms that integrate Internet of Things (IoT) systems and online services, rich functionalities transparently connecting digital physical worlds become easily accessible for the end users. On other hand, such facilities incorporate multiple parties whose data control policies may radically differ even contradict each other, thus privacy violations arise throughout lifecycle (e.g., generation transmission) triggers actions. In this work, we conduct an in-depth...

The actual driving conditions of electric vehicles (EVs) are complex and changeable. Limited by road adhesion conditions, it is necessary to give priority ensuring safety, taking into account the energy recovery ratio vehicle during braking obtain better quality. In this work, an with EHB (electro-hydraulic braking) system whose force adaptive distribution control strategy studied. Firstly, dynamics model, including seven degrees freedom, tire, drive motor, main reducer, battery pack,...

Hybrid systems model checking is a great success in guaranteeing the safety of computerized control cyber-physical (CPS). However, when applying hybrid to Medical Device Plug-and-Play(MDPnP) CPS, we encounter two challenges due complexity human body: i) there are no good offline differential equation based models for many body parameters, ii) can result variables, complicating system model. In an attempt address challenges, propose alter traditional approach time-unbounded (i.e., long-run)...

Reachability analysis of linear hybrid automata (LHA) is an important problem. Classical model checking (CMC) technique not scalable and guaranteed to terminate. On the other hand, bounded (BMC) more cost-effective conduct but can guarantee safety beyond bound. In this paper, we seek bridge gap between BMC CMC for reachability LHA. During LHA, typical procedures discover sets unsatisfiable constraint cores, which be mapped back path segments in graph structure If every connecting initial...

Neural network based (NN-based) classifiers are known vulnerable against adversarial examples, namely, adding slight perturbations to a benign image cause classifier make false prediction. To evaluate the robustness of NN-based numerous attacks with high success rates have been proposed recently. usually normalize valid images (e.g., RGB where value at each coordinate is an integer between 0 and 255) into real continuous domain 3-dimensional matrix number 1) classification decisions on...

The existing techniques for reachability analysis of linear hybrid automata do not scale well to problem sizes practical interest. Instead developing a tool perform check on all the paths automaton, complementary approach is develop an efficient path-oriented one path at time where length being checked can be made very large and size automaton enough handle problems This symbolic execution used by design engineers important thereby, increase faith in correctness system. Unlike simple...

Cyber-Physical Systems (CPS) integrate discretetime computing and continuous-time physical-world entities, which are often wirelessly interlinked.The use of wireless safety critical CPS (control, healthcare etc.) requires guarantees despite communication faults.This paper focuses on one important set such rules: Proper-Temporal-Embedding (PTE).Our solution introduces hybrid automata to formally describe analyze design patterns.We propose a novel lease based pattern, along with closed-form...

Ordinary users can build their smart home automation system easily nowadays, but such user-customized systems could be error-prone. Using formal verification to prove the correctness of is necessary. However, conduct proof, specifications as Linear Temporal Logic (LTL) formulas have provided, ordinary cannot author LTL only natural language.To address this problem, paper presents a novel approach that automatically generate from language requirements based on domain knowledge and our...

TVM is a popular deep learning (DL) compiler. It designed for compiling DL models, which are naturally computation graphs, and as well promoting the efficiency of computation. State-of-the-art methods, such Muffin NNSmith, allow developers to generate graphs testing compilers. However, these techniques inefficient — their generated either type-invalid or inexpressive, hence not able test core functionalities

Wireless Sensor Networks (WSNs) are widely used in different kinds of environments. They may encounter lots stochastic uncertainties and disturbances like message loss node dynamics. Thus, it is critical to ensure the correctness low level protocols WSNs evaluate their performance under circumstances. In this paper, we propose a new method analyze WSN based on timed automata statistical model checking. For modeling, work flow protocol can be modeled with classical automata. Then, such as...

Mobile applications with complex GUIs are very popular today. However, generating test cases for these is often tedious professional work. On the one hand, manually designing and writing elaborate GUI scripts requires expertise. other record playback techniques usually depends on repetitive work that testers need to interact application over again, because only path recorded in an execution. Automatic testing focuses exploring combinations of events. As number huge, it still necessary...

Cyber-Physical Systems (CPS) integrate discrete-time computing and continuous-time physical-world entities, which are often wirelessly interlinked. The use of wireless safety-critical CPS requires safety guarantees despite communication faults. This paper focuses on one important set such rules: Proper-Temporal-Embedding (PTE), where distributed entities must enter/leave risky states according to properly nested temporal pattern certain duration spacing. Our solution introduces hybrid...

Acute pain is a prevalent problem for dementia residents in nursing homes. A variety of intervention strategies have been applied to address this problem. However, there remains an issue inadequate control. This study aims explore the analgesic efficacy auricular acupressure (AA) with acute homes.A multicenter, single-blind, randomized, and sham-controlled clinical trial was performed three homes Yinchuan, China. All 206 eligible patients were randomly divided into two groups real AA therapy...