-
Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification
Authors:
Márk Somorjai,
Mihály Dobos-Kovács,
Zsófia Ádám,
Levente Bajczi,
András Vörös
Abstract:
Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification. Most existing solvers use a diverse set of specialized techniques, including direct state space traversal or under-approximating abstraction, necessitating purpose-built complex algorithms. Other solvers successfully simplified the verification workflow by translating the problem to…
▽ More
Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification. Most existing solvers use a diverse set of specialized techniques, including direct state space traversal or under-approximating abstraction, necessitating purpose-built complex algorithms. Other solvers successfully simplified the verification workflow by translating the problem to inputs for other verification tasks, leveraging the strengths of existing algorithms. One such approach transforms the CHC problem into a recursive program roughly emulating a top-down solver for the deduction task; and verifying the reachability of a safety violation specified as a control location. We propose an alternative bottom-up approach for linear CHCs, and evaluate the two options in the open-source model checking framework THETA on both synthetic and industrial examples. We find that there is a more than twofold increase in the number of solved tasks when the novel bottom-up approach is used in the verification workflow, in contrast with the top-down technique.
△ Less
Submitted 23 April, 2024;
originally announced April 2024.
-
Towards formally analyzed Cyber-Physical Systems
Authors:
Richárd Szabó,
András Vörös
Abstract:
Cyber-physical systems (CPS) can be found everywhere: smart homes, autonomous vehicles, aircrafts, healthcare, agriculture and industrial production lines. CPSs are often critical, as system failure can cause serious damage to property and human lives. Today's cyber-physical systems are extremely complex, heterogeneous systems: to be able to manage their complexity in a unified way, we need an inf…
▽ More
Cyber-physical systems (CPS) can be found everywhere: smart homes, autonomous vehicles, aircrafts, healthcare, agriculture and industrial production lines. CPSs are often critical, as system failure can cause serious damage to property and human lives. Today's cyber-physical systems are extremely complex, heterogeneous systems: to be able to manage their complexity in a unified way, we need an infrastructure that ensures that our systems operate with the high reliability as intended. In addition to the infrastructure, we need to provide engineers a method to ensure system reliability at design time. The paradigm of model-driven design provides a toolkit supporting the design and analysis and by choosing the proper formalisms, the model-driven design approach allows us to validate our system at design time.
△ Less
Submitted 29 August, 2021;
originally announced August 2021.
-
Simulation-based Safety Assessment of High-level Reliability Models
Authors:
Simon József Nagy,
Bence Graics,
Kristóf Marussy,
András Vörös
Abstract:
Systems engineering approaches use high-level models to capture the architecture and behavior of the system. However, when safety engineers conduct safety and reliability analysis, they have to create formal models, such as fault-trees, according to the behavior described by the high-level engineering models and environmental/fault assumptions. Instead of creating low-level analysis models, our ap…
▽ More
Systems engineering approaches use high-level models to capture the architecture and behavior of the system. However, when safety engineers conduct safety and reliability analysis, they have to create formal models, such as fault-trees, according to the behavior described by the high-level engineering models and environmental/fault assumptions. Instead of creating low-level analysis models, our approach builds on engineering models in safety analysis by exploiting the simulation capabilities of recent probabilistic programming and simulation advancements. Thus, it could be applied in accordance with standards and best practices for the analysis of a critical automotive system as part of an industrial collaboration, while leveraging high-level block diagrams and statechart models created by engineers. We demonstrate the applicability of our approach in a case study adapted from the automotive system from the collaboration.
△ Less
Submitted 28 April, 2020;
originally announced April 2020.
-
Why Do Men Get More Attention? Exploring Factors Behind Success in an Online Design Community
Authors:
Johannes Wachs,
Anikó Hannák,
András Vörös,
Bálint Daróczy
Abstract:
Online platforms are an increasingly popular tool for people to produce, promote or sell their work. However recent studies indicate that social disparities and biases present in the real world might transfer to online platforms and could be exacerbated by seemingly harmless design choices on the site (e.g., recommendation systems or publicly visible success measures). In this paper we analyze an…
▽ More
Online platforms are an increasingly popular tool for people to produce, promote or sell their work. However recent studies indicate that social disparities and biases present in the real world might transfer to online platforms and could be exacerbated by seemingly harmless design choices on the site (e.g., recommendation systems or publicly visible success measures). In this paper we analyze an exclusive online community of teams of design professionals called Dribbble and investigate apparent differences in outcomes by gender. Overall, we find that men produce more work, and are able to show it to a larger audience thus receiving more likes. Some of this effect can be explained by the fact that women have different skills and design different images. Most importantly however, women and men position themselves differently in the Dribbble community. Our investigation of users' position in the social network shows that women have more clustered and gender homophilous following relations, which leads them to have smaller and more closely knit social networks. Overall, our study demonstrates that looking behind the apparent patterns of gender inequalities in online markets with the help of social networks and product differentiation helps us to better understand gender differences in success and failure.
△ Less
Submitted 8 May, 2017;
originally announced May 2017.
