Online dating has transformed the way in which modern romance is perceived. As a consequence, creating trust on these digital platforms has become more important than ever before. One of the most popular ways to enhance users’ trust in digital settings is the process of verification, followed by obtaining a verification badge as a result. These icons have an established meaning that the user to which they belong has verified their identity. Yet, the influence that the design of verification badges on dating applications has on users’ trust remains unknown. In this thesis, the impact of badge design elements, specifically color and shape on users’ trust will be explored with the use of an online semi-structured survey. Participants are presented with three badge designs, differing in color and shape, prompting them to evaluate their perceived trustworthiness. By incorporating both qualitative and quantitative data, the research enables a mix of a comprehensive analysis of answers to open-ended questions that allow for a deeper understanding of the reasoning behind made choices, and a thorough examination of the close-ended ones, which represent the perceptions statistically. Through descriptive statistical analysis of quantitative data and thematic analysis of qualitative responses, this study aims to find patterns and correlations among the badges’ design attributes that enhance users’ trust. The results of this research strive to enhance comprehension of the influence that design elements have on user perceptions of trust within digital platforms, specifically within the domain of online dating applications. The results from this study show that both color and shape have an impact on trust between users and are heavily impacted by familiarity. This means that it is necessary to use them appropriately when designing dating application interfaces, to avoid confusion and increase the perceptions of trust. Findings also show that women tend to pay greater attention to the design of verification badges compared to men. The knowledge gained in this research may guide the enhancement of verification badge systems, promoting trust and assurance among online daters.

No description available.

In this dissertation, we study the verification of concurrent programs written in the programming language Erlang using infinite-state model-checking. Erlang is a widely used, higher order, dynamically typed, call-by-value functional language with algebraic data types and pattern-matching. It is further augmented with support for actor concurrency, i.e. asynchronous message passing and dynamic process creation. With decidable model-checking in mind, we identify actor communicating systems (ACS) as a suitable target model for an abstract interpretation of Erlang. ACS model a dynamic network of finite-state processes that communicate over a fixed, finite number of unordered, unbounded channels. Thanks to being equivalent to Petri nets, ACS enjoy good algorithmic properties. We develop a verification procedure that extracts a sound abstract model, in the form of an ACS, from a given Erlang program; the resulting ACS simulates the operational semantics of the input. Using this abstract model, we can conservatively verify coverability properties of the input program, i.e. a weak form of safety properties, with a Petri net model-checker. We have implemented this procedure in our tool Soter, which is the first sound verification tool for Erlang programs using infinite-state model-checking. In our experiments, we find that Soter is accurate enough to verify a range of interesting and non-trivial benchmarks. Even though ACS coverability is Expspace-complete, Soter's analysis of these verification problems is surprisingly quick. In order to improve the precision of our verification procedure with respect to recursion, we investigate an extension of ACS that allows pushdown processes: asynchronously communicating pushdown systems (ACPS). ACPS that satisfy the empty-stack constraint (a pushdown process may receive only when its stack is empty) are a popular subclass of ACPS with good decision and complexity properties. In the context of Erlang, the empty stack constraint is unfortunately not realistic. We introduce a relaxation of the empty-stack constraint for ACPS called the shaped stack constraint. Stacks that fit the shape constraint may reach arbitrary heights. Further, a process may execute any communication action (be it process creation, message send or retrieval) whether or not its stack is empty. We prove that coverability for shaped ACPS, i.e. ACPS that satisfy the shaped constraint, reduces to the decidable coverability problem for well-structured transition systems (WSTS). Thus, shaped ACPS enable the modelling and verification of a larger class of message passing programs. We establish a close connection between shaped ACPS and a novel extension of Petri nets: nets with nested coloured tokens (NNCT). Tokens in NNCT are of two types: simple and complex. Complex tokens carry an arbitrary number of coloured tokens. The rules of a NNCT can synchronise complex and simple tokens, inject coloured tokens into a complex token, and eject all tokens of a specified set of active colours to predefined places. We show that the coverability problem for NNCT is Tower-complete, a new complexity class for non-elementary decision problems introduced by Schmitz. To prove Tower-membership, we devise a geometrically inspired version of the Rackoff technique, and we obtain Tower-hardness by adapting Stockmeyer's ruler construction to NNCT. To our knowledge, NNCT is the first extension of Petri nets (belonging to the class of nets with an infinite set of token types) that is proven to have primitive recursive coverability. This result implies Tower-completeness of coverability for ACPS that satisfy the shaped stack constraint.

Made available in DSpace on 2014-12-17T14:55:40Z (GMT). No. of bitstreams: 1 AdautoLT.pdf: 2061017 bytes, checksum: 12a139ba25174e3b22d08cf31c934500 (MD5) Previous issue date: 2009-09-04 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / This work proposes a new methodology to verify those analog circuits, providing an automated tools to help the verifiers to have a more truthful result. This work presents the development of new methodology for analog circuits verification. The main goal is to provide a more automated verification process to certify analog circuits functional behavior. The proposed methodology is based on the golden model technique. A verification environment based on this methodology was built and results of a study case based on the validation of an operational amplifier design are offered as a confirmation of its effectiveness. The results had shown that the verification process was more truthful because of the automation provided by the tool developed / O presente trabalho tem como objetivo desenvolver uma ferramenta de verifica??o para circuitos anal?gicos. O principal objetivo desta ? aumentar a automa??o dos processos de verifica??o. Al?m disso, proporcionar a constru??o de um ambiente de verifica??o capaz de gerar relat?rios ao longo deste processo. Esta metodologia ? baseada na t?cnica do Modelo de Ouro, no entanto, ela tamb?m prop?e uma segunda t?cnica para verificar o modelo de refer?ncia, para se obter resultados mais confi?veis. A metodologia foi utilizada, como estudo de caso, na verifica??o de um amplificador operacional

Thesis (MSc)--University of Stellenbosch, 2007. / ENGLISH ABSTRACT: Computer aided veri cation techniques, such as model checking, can be used to improve the reliability of software. Model checking is an algorithmic approach to illustrate the correctness of temporal logic speci cations in the formal description of hardware and software systems. In contrast to traditional testing tools, model checking relies on an exhaustive search of all the possible con gurations that these systems may exhibit. Traditionally model checking is applied to abstract or high level designs of software. However, often interpreting or translating these abstract designs to implementations introduce subtle errors. In recent years one trend in model checking has been to apply the model checking algorithm directly to the implementations instead. This thesis is concerned with building an e cient model checker for a small concurrent langauge developed at the University of Stellenbosch. This special purpose langauge, LF, is aimed at developement of small embedded systems. The design of the language was carefully considered to promote safe programming practices. Furthermore, the language and its runtime support system was designed to allow directly model checking LF programs. To achieve this, the model checker extends the existing runtime support infrastructure to generate the state space of an executing LF program. / AFRIKAANSE OPSOMMING: Rekenaar gebaseerde program toetsing, soos modeltoetsing, kan gebruik word om die betroubaarheid van sagteware te verbeter. Model toetsing is 'n algoritmiese benadering om die korrektheid van temporale logika spesi kasies in die beskrywing van harde- of sagteware te bewys. Anders as met tradisionlee program toetsing, benodig modeltoetsing 'n volledige ondersoek van al die moontlike toestande waarin so 'n beskrywing homself kan bevind. Model toetsing word meestal op abstrakte modelle van sagteware of die ontwerp toegepas. Indien die ontwerp of model aan al die spesi kasies voldoen word die abstrakte model gewoontlik vertaal na 'n implementasie. Die vertalings proses word gewoontlik met die hand gedoen en laat ruimte om nuwe foute, en selfs foute wat uitgeskakel in die model of ontwerp is te veroorsaak. Deesdae, is 'n gewilde benadering tot modeltoetsing om di e tegnieke direk op die implementasie toe te pas, en sodoende die ekstra moeite van model konstruksie en vertaling uit te skakel. Hierdie tesis handel oor die ontwerp, implementasie en toetsing van 'n e ektiewe modeltoetser vir 'n klein gelyklopende taal, LF, wat by die Universiteit van Stellenbosch ontwikkel is. Die enkeldoelige taal, LF, is gemik op die veilige ontwikkeling van ingebedde sagteware. Die taal is ontwerp om veilige programmerings praktyke aan te moedig. Verder is die taal en die onderliggende bedryfstelsel so ontwerp om 'n model toetser te akkomodeer. Om die LF programme direk te kan toets, is die model toetser 'n integrale deel van die bedryfstelsel sodat dit die program kan aandryf om alle moontlike toestande te besoek.

Pushdown systems equip a finite state system with an unbounded stack memory, and are thus infinite state. By recording the call history on the stack, these systems provide a natural model for recursive procedure calls. Model-checking for pushdown systems has been well-studied. Tools implementing pushdown model-checking (e.g. Moped) are an essential back-end component of high-profile software model checkers such as SLAM, Blast and Terminator. Higher-order pushdown systems define a more complex memory structure: a higher-order stack is a stack of lower-order stacks. These systems form a robust hierarchy closely related to the Caucal hierarchy and higher-order recursion schemes. This latter connection demonstrates their importance as models for programs with higher-order functions. We study the global model-checking problem for (higher-order) pushdown systems. In particular, we present a new algorithm for computing the winning regions of a parity game played over an order-1 pushdown system. We then show how to compute the winning regions of two-player reachability games over order-n pushdown systems. These algorithms extend the saturation methods of Bouajjani, Esparza and Maler for order-1 pushdown systems, and Bouajjani and Meyer for higher-order pushdown systems with a single control state. These techniques begin with an automaton recognising (higher-order) stacks, and iteratively add new transitions until the automaton becomes saturated. The reachability result, presented at FoSSaCS 2007 and in the LMCS journal, is the main contribution of the thesis. We break the saturation paradigm by adding new states to the automaton during the iteration. We identify the fixed points required for termination by tracking the updates that are applied, rather than by observing the transition structure. We give a number of applications of this result to LTL model-checking, branching-time model-checking, non-emptiness of higher-order pushdown automata and Büchi games. Our second major contribution is the first application of the saturation technique to parity games. We begin with a mu-calculus characterisation of the winning region. This formula alternates greatest and least fixed point operators over a kind of reachability formula. Hence, we can use a version of our reachability algorithm, and modifications of the Büchi techniques, to compute the required result. The main advantages of this approach compared to existing techniques due to Cachat, Serre and Vardi et al. are that it is direct and that it is not immediately exponential in the number of control states, although the worst-case complexity remains the same.

The Parameterised Model Checking Problem asks whether an implementation Impl(t) satisfies a specification Spec(t) for all instantiations of parameter t. In general, t can determine numerous entities: the number of processes used in a network, the type of data, the capacities of buffers, etc. The main theme of this thesis is automation of uniform verification of a subclass of PMCP with the parameter of the first kind, using techniques based on counter abstraction. Counter abstraction works by counting how many, rather than which, node processes are in a given state: for nodes with k local states, an abstract state (c(1), ..., c(k)) models a global state where c(i) processes are in the i-th state. We then use a threshold function z to cap the values of each counter. If for some i, counter c(i) reaches its threshold, z(i) , then this is interpreted as there being z(i) or more nodes in the i-th state. The addition of thresholds makes abstract models independent of the instantiation of the parameter. We adapt standard counter abstraction techniques to concurrent reactive systems modelled using the CSP process algebra. We demonstrate how to produce abstract models of systems that do not use node identifiers (i.e. where all nodes are indistinguishable). Every such abstraction is, by construction, refined by all instantiations of the implementation. If the abstract model satisfies the specification, then a positive answer to the particular uniform verification problem can be deduced. We show that by adding node identifiers we make the uniform verification problem undecidable. We demonstrate a sound abstraction method that extends standard counter abstraction techniques to systems that make full use of node identifiers (in specifications and implementations). However, on its own, the method is not enough to give the answer to verification problems for all parameter instantiations. This issue has led us to the development of a type reduction theory, which, for a given verification problem, establishes a function phi that maps all (sufficiently large) instantiations T of the parameter to some fixed type T and allows us to deduce that if Spec(T) is refined by phi(Impl(T)), then Spec(T) is refined by Impl(T). We can then combine this with our extended counter abstraction techniques and conclude that if the abstract model satisfies Spec(T), then the answer to the uniform verification problem is positive. We develop a symbolic operational semantics for CSP processes that satisfy certain normality requirements and we provide a set of translation rules that allow us to concretise symbolic transition graphs. The type reduction theory relies heavily on these results. One of the main advantages of our symbolic operational semantics and the type reduction theory is their generality, which makes them applicable in other settings and allows the theory to be combined with abstraction methods other than those used in this thesis. Finally, we present TomCAT, a tool that automates the construction of counter abstraction models and we demonstrate how our results apply in practice.

Probabilistic model checking is a powerful formal verification method that can ensure the correctness of real-life systems that exhibit stochastic behaviour. The work presented in this thesis aims to solve the scalability challenge of probabilistic model checking, by developing, for the first time, fully-automated compositional verification techniques for probabilistic systems. The contributions are novel approaches for automatically learning probabilistic assumptions for three different compositional verification frameworks. The first framework considers systems that are modelled as Segala probabilistic automata, with assumptions captured by probabilistic safety properties. A fully-automated approach is developed to learn assumptions for various assume-guarantee rules, including an asymmetric rule Asym for two-component systems, an asymmetric rule Asym-N for n-component systems, and a circular rule Circ. This approach uses the L* and NL* algorithms for automata learning. The second framework considers systems where the components are modelled as probabilistic I/O systems (PIOSs), with assumptions represented by Rabin probabilistic automata (RPAs). A new (complete) assume-guarantee rule Asym-Pios is proposed for this framework. In order to develop a fully-automated approach for learning assumptions and performing compositional verification based on the rule Asym-Pios, a (semi-)algorithm to check language inclusion of RPAs and an L*-style learning method for RPAs are also proposed. The third framework considers the compositional verification of discrete-time Markov chains (DTMCs) encoded in Boolean formulae, with assumptions represented as Interval DTMCs (IDTMCs). A new parallel operator for composing an IDTMC and a DTMC is defined, and a new (complete) assume-guarantee rule Asym-Idtmc that uses this operator is proposed. A fully-automated approach is formulated to learn assumptions for rule Asym-Idtmc, using the CDNF learning algorithm and a new symbolic reachability analysis algorithm for IDTMCs. All approaches proposed in this thesis have been implemented as prototype tools and applied to a range of benchmark case studies. Experimental results show that these approaches are helpful for automating the compositional verification of probabilistic systems through learning small assumptions, but may suffer from high computational complexity or even undecidability. The techniques developed in this thesis can assist in developing scalable verification frameworks for probabilistic models.

Alternating timed automata are a powerful extension of classical Alur-Dill timed automata that are closed under all Boolean operations. They have played a key role, among others, in providing verification algorithms for prominent specification formalisms such as Metric Temporal Logic. Unfortunately, when interpreted over an infinite dense time domain (such as the reals), alternating timed automata have an undecidable language emptiness problem. In this thesis we consider restrictions on this model that restore the decidability of the language emptiness problem. We consider the restricted class of safety alternating timed automata, which can encode a corresponding Safety fragment of Metric Temporal Logic. This thesis connects these two formalisms with insertion channel machines, a model of faulty communication, and demonstrates that the three formalisms are interreducible. We thus prove a non-elementary lower bound for the language emptiness problem for 1-clock safety alternating timed automata and further obtain a new proof of decidability for this problem. Complementing the restriction to safety properties, we consider interpreting the automata over bounded dense time domains. We prove that the time-bounded language emptiness problem is decidable but non-elementary for unrestricted alternating timed automata. The language emptiness problem for alternating timed automata is a special case of a much more general and abstract logical problem: Church's synthesis problem. Given a logical specification S(I,O), Church's problem is to determine whether there exists an operator F that implements the specification in the sense that S(I,F(I)) holds for all inputs I. It is a classical result that the synthesis problem is decidable in the case that the specification and implementation are given in monadic second-order logic over the naturals. We prove that this decidability extends to MSO over the reals with order and furthermore to MSO over every fixed bounded interval of the reals with order and the +1 relation.

Model checking is an automatic formal verification technique for establishing correctness of systems. It has been widely used in industry for analysing and verifying complex safety-critical systems in application domains such as avionics, medicine and computer security, where manual testing is infeasible and even minor errors could have dire consequences. In our increasingly parallelised world, concurrency has become pivotal and seamlessly woven within programming paradigms, however, extremely challenging when it comes to modelling and establishing correctness of intended behaviour. Tools for model checking concurrent systems face severe limitations due to scalability problems arising from the need to examine all possible interleavings (schedules) of executions of parallel components. Moreover, concurrency poses additional challenges to model checking, giving rise to phenomena such as nondeterminism, deadlock, livelock, etc. In this thesis we focus on adapting and developing novel model-checking techniques for concurrent systems in the setting of the process algebra CSP and its primary model checker FDR. CSP allows for a compact modelling and precise analysis of event-based concurrency, grounded on synchronous message passing as a fundamental mechanism of inter-component communication. In particular, we investigate techniques based on symbolic model checking, static analysis and abstraction, all of them exploiting the compositionality inherent in CSP and targeting to increase the scale of systems that can be tractably analysed. Firstly, we investigate symbolic model-checking techniques based on Boolean satisfiability (SAT), which we adapt for the traces model of CSP. We tailor bounded model checking (BMC), that can be used for bug detection, and temporal k-induction, which aims at establishing inductiveness of properties and is capable of both bug finding and establishing the correctness of systems. Secondly, we propose a static analysis framework for establishing livelock freedom of CSP processes, with lessons for other concurrent formalisms. As opposed to traditional exhaustive state-space exploration, our framework employs a system of rules on the syntax of a process to calculate a sound approximation of its fair/co-fair sets of events. The rules either safely classify a process as livelock-free or report inconclusiveness, thereby trading accuracy for speed. Finally, we develop a series of abstraction/refinement schemes for the traces, stable-failures and failures-divergences models of CSP and embed them into a fully automated and compositional CEGAR framework. For each of those techniques we present an implementation and an experimental evaluation on a set of CSP benchmarks.