Wishnu Prasetya

Researcher at the Software Technology group, Dept. of Information & Computing Sciences, Utrecht University.

Research interest: software verification, automated software testing, automated debugging.


What I am working on lately:

[01-09-2014] I am working on test suites query and manipulation library on top T3. We have now LTL and algebraic queries on test suites generated by T3. Working on oracles-inference, and sub-cases splitters...
svn



Collection of My Papers

Reduce First, Debug Later, A. Elyasov, I.S.W.B. Prasetya, J. Hage, A. Nikas, in the 9th International Workshop on Automation of Software Test, ACM, 2014. The delta debugging minimization algorithm ddmin provides an efficient procedure for the simplification of failing test-cases. Despite its contribution towards the automation of debugging, ddmin still requires a significant number of iterations to complete. The delta debugging (DD) search space can be narrowed down by providing the test-case circumstances that are most likely relevant to the occurred failure. This paper proposes a novel approach to the problem of failure simplification consisting of two consecutive phases: 1) failure reduction by rewriting (performed offline), and 2) DD invocation (performed online). In the best case scenario, the reduction phase may already deliver a simplified failure, otherwise, it potentially supplies DD with extra information about where to look for the failure. The proposed solution has been prototyped as a web application debugging tool, which was evaluated on a shopping cart web application - Flex Store. The evaluation shows an improvement of the DD execution time if the offline reduction over-approximates the failure.
FITTEST: A New Continuous and Automated Testing Process for Future Internet Applications, T.E.J. Vos, P. Tonella, I.S.W.B. Prasetya, P.M. Kruse, A. Bagnato, M. Harman, O. Shehory, in the Conf. on Software Maintenance, Reengineering and Reverse Engineering (CSMR-WCRE), IEEE, 2014. Since our society is becoming increasingly dependent on applications emerging on the Future Internet, quality of these applications becomes a matter that cannot be neglected. However, the complexity of the technologies involved in Future Internet applications makes testing extremely challenging. The EU FP7 FITTEST project has addressed some of these challenges by developing and evaluating a Continuous and Integrated Testing Environment that monitors a Future Internet application when it runs such that it can automatically adapt the testware to the dynamically changing behaviour of the application.
The FITTEST Tool Suite for Testing Future Internet Applications, T.E.J. Vos, P. Tonella, I.S.W.B. Prasetya, P.M. Kruse, O. Shehory, A. Bagnato, M. Harman, in the Int. Workshop Future Internet Testing, LNCS 8432, Springer, 2014. Future Internet applications are expected to be much more complex and powerful, by exploiting various dynamic capabilities For testing, this is very challenging, as it means that the range of possible behavior to test is much larger, and moreover it may at the run time change quite frequently and significantly with respect to the assumed behavior tested prior to the release of such an application. The traditional way of testing will not be able to keep up with such dynamics. The Future Internet Testing (FITTEST) project (http://crest.cs.ucl.ac.uk/fittest/), a research project funded by the European Commission (grant agreement n. 257574) from 2010 till 2013, was set to explore new testing techniques that will improve our capacity to deal with the challenges of testing Future Internet applications. Such techniques should not be seen as replacement of the traditional testing, but rather as a way to complement it. This paper gives an overview of the set of tools produced by the FITTEST project, implementing those techniques.
T3, a Combinator-based Random Testing Tool for Java: Benchmarking, I.S.W.B. Prasetya, in the Int. Workshop Future Internet Testing, LNCS 8432, Springer, 2014. T3 is the next generation of the light weight automated testing tool T2 for Java. In the heart T3 is still a random testing tool; but it now comes with some new features: pair-wise testing, concurrent generators, and a combinator-based approach ala QuickCheck. This paper presents the result of benchmarking of T3 on its default configuration against a set of real world classes.
Logging to Facilitate Combinatorial System Testing, P.M. Kruse, I.S.W.B. Prasetya, J. Hage, A. Elyasov, in the Int. Workshop Future Internet Testing, LNCS 8432, Springer, 2014. Testing a web application is typically very complicated. Imposing simple coverage criteria such as function or line coverage is often not sufficient to uncover bugs due to incorrect components integration. Combinatorial testing can enforce a stronger criterion, while still allowing the prioritization of test cases in order to keep the overall effort feasible. Combinatorial testing requires the whole testing domain to be classified and formalized, e.g., in terms of classification trees. At the system testing level, these trees can be quite large. This short paper presents our preliminary work to automatically construct classification trees from loggings of the system, and to subsequently calculate the coverage of our test runs against various combinatorial criteria. We use the tool CTE which allows such criteria to be custom specified. Furthermore, it comes with a graphical interface to simplify the specification of new test sequences.
Guided Algebraic Specification Mining for Failure Simplification, A. Elyasov, I.S.W.B. Prasetya, J. Hage, in the 25th IFIP International Conference on Testing Software and Systems (ICTSS), LNCS 8254, Springer, 2013. Software systems often produce logs that capture information about their execution behaviour. When an error occurs, the log file with the error is reported for subsequent analysis. The longer the log file, the harder to identify the cause of the observed error. This problem can be considerably simplified if we reduce the log length, e.g., by removing events which do not contribute towards finding the error. This paper addresses the problem of log reduction by rewriting the reported log in such a way that it preserves the ability to reproduce the same error. The approach exploits rewrite rules inferred from a set of predefined algebraic rewrite rule patterns, exhibiting such properties as commutativity and identity. The paper presents an algorithm for rewrite rules inference, and a terminating reduction strategy based on these rules. Being log-based the inference algorithm is inherently imprecise. So the inferred rules need to be inspected by a human expert before actually being used for rewriting. The approach is language independent and highly flexible. The paper formally defines all used concepts and discusses a prototype implementation of a log reduction framework. The prototype was empirically validated on a web shop application.
Compact Traceable Logging, I.S.W.B. Prasetya, A. Sturala, A. Middelkoop, J. Hage, A. Elyasov, in the 5th International Conference on Advances in System Testing and Validation Lifecycle (VALID), 2013. We present a source code transformation scheme that converts the given program with ordinary logging to enhance it with tracing information, and at the same time significantly reduces the size of the generated logs by applying a form of binary encoding. Decoders are generated to interpret the logs and establish how the executions that produced them flowed through relevant decision branches in the program. The paper describes the transformation for sizeable subset of sequential Java, including its complicated control structures. Prototype
Measuring T2 against SBST 2013 Benchmark Suite, I.S.W.B. Prasetya, in the Proc. of Software Testing Verification and Validation (ICST) Workshops, IEEE, 2013.
Testing of Future Internet Applications Running in the Cloud, T.E.J. Vos, P. Tonella, J. Wegener, M. Harman, I.S.W.B. Prasetya, S. Ur, in Software Testing in the Cloud: Perspectives on an Emerging Discipline. S. Tilley, T. Parveen (Eds.), IGI Global, 2012. The cloud will be populated by software applications that consist of advanced, dynamic, and largely autonomic interactions among services, end-user applications, content, and media. The complexity of the technologies involved in the cloud makes testing extremely challenging and demands novel approaches and major advancements in the field. This chapter describes the main challenges associated with the testing of applications running in the cloud. The authors present a research agenda that has been defined in order to address the testing challenges. The goal of the agenda is to investigate the technologies for the development of an automated testing environment, which can monitor the applications under test and can react dynamically to the observed changes. Realization of this environment involves substantial research in areas such as search based testing, model inference, oracle learning, and anomaly detection.
FITTEST Log Format (version 1.1), I.S.W.B. Prasetya, A. Elyasov, A. Middelkoop, J. Hage, Technical report UU-CS-2012-014, Dept. of Information and Computing Sciences, Utrecht University, 2012. This report describes the FITTEST log format. "FITTEST" is the name of the project from where the format originates, which stands for Future Internet Testing. The format itself has nothing to do with Internet; it can be used to express any kind of logs. The important feature of the FITTEST format is that is deeply structured ala XML. However, it is more compact (in our examples, by a factor of 2). As in XML, log entries are tagged.
Using Sub-cases to Improve Log-based Oracles Inference, I.S.W.B. Prasetya, J. Hage, A. Elyasov, Technical report UU-CS-2012-012, Dept. of Information and Computing Sciences, Utrecht University, 2012. Reverse engineering of test-oracles is a notoriously hard problem. A well known approach (Daikon) is to learn pre- and post-conditions from logs. However, the expressiveness of the formulas that can be inferred is very limited. This paper explains an translation scheme for a new class of oracles called word oracles, so that they can be inferred with Daikon. The insight behind it is that the various behavior of a program can often be grouped into a number of 'behavior classes'. Logs can be regrouped, so that oracles are inferred with respect to each of these classes. By definition these oracles are stronger. The trade off is that we have to specify the behavior classes ourselves. Word oracles allow the behavior classes to be defined as patterns over the sequences of event names (rather than the events themselves). This is reasonably powerful, and e.g. regular expressions can be used to express the patterns. We have implemented a prototype, and we are currently working on validating it on a case study, and improving it.
Log-Based Reduction by Rewriting, A. Elyasov, I.S.W.B. Prasetya, J. Hage, Technical report UU-CS-2012-013, Dept. of Information and Computing Sciences, Utrecht University, 2012. —Software systems often produce logs which contain information about the execution of the systems. When an error occurs, the log file with the error is reported for subsequent analysis. The longer the log file, the harder to identify the cause of the observed error. This problem can be considerably simplified, if we reduce the log length, e.g., by removing events which do not contribute towards finding the error. This paper addresses the problem of log reduction by rewriting the reported log in such a way that it preserves the ability to reproduce the same error. The approach exploits rewrite rules inferred from a set of predefined algebraic rewrite rule patterns, capturing such properties as commutativity and identity. The paper presents an algorithm for inferencing the rewrite rules from logs and a terminating reduction strategy based on these rules. Being log-based the inference algorithm is inherently imprecise. So the inferred rules need to be inspected by an expert before actually being used for rewriting. The approach is language independent and highly flexible. The paper formally defines all used concepts and discusses a prototype implementation of a log reduction framework. The prototype was empirically validated on a web shop application.
Functional Instrumentation of ActionScript Programs with ASIL, A. Middelkoop, A. Elyasov, I.S.W.B. Prasetya, in Proc. Symposium on Implementation and Application of Functional Language (IFL), Springer, 2011. , "Within the context of the FITTEST project, one of our tasks was to instrument ActionScript bytecode, so that aspects of the execution of the running application are logged. Although the decision what to log and when requires manual intervention, the code itself can be weaved into the system automatically by means of aspect-oriented programming (AOP). In this paper we describe Asil, an AOP EDSL for instrumenting ActionScript bytecode, that is firmly based on well-known functional programming technique to provide abstraction mechanisms that other AOP languages tend to lack."
Using Haskell to Script Combinatoric Testing of Web Services, I.S.W.B. Prasetya, J. Amorim, T.E.J. Vos, A. Baars, in Proc. 6th Iberian Conference on Information Systems and Technologies (CISTI), IEEE, 2011. he Classification Tree Method (CTM) is a popular approach in functional testing as it allows the testers to systematically partition the input domain of an SUT, and specifies the combinations they want. We have implemented the approach as a small domain specific language (DSL) embedded in the functional language Haskell. Such an embedding leads to clean syntax and moreover we can natively access Haskell's full features. This paper will explain the approach, and how it is applied for testing Web Services.

Earlier versions (free):

CTy: a Haskell DSL for Specifying and Generating Combinatoric Test-cases, I.S.W.B. Prasetya, J. Amorim, T.E.J. Vos, A. Baars, Tech. Report UU-CS-2011-005, Dept. of Information and Computing Sciences, Utrecht University, 2011.
Future Internet Testing with FITTEST, T.E.J. Vos, P. Tonella, J. Wegener, M. Harman, I.S.W.B. Prasetya, E. Puoskari, Y. Nir-Buchbinder, {\it }, in Proc. 15th European Conference on Software Maintenance and Reengineering (CSMR), IEEE, 2011. The complexity of the technologies involved in the Future Internet makes testing extremely challenging and demands for novel approaches and major advancement in the field. The overall aim of the FITTEST project is to address these testing challenges, by developing an integrated environment for automated testing, which can monitor the Future Internet application under test and adapt to the dynamic changes observed. Future Internet applications do not remain fixed after their release, services and components can be dynamically added by customers. Consequently, FITTEST testing will be continuous and post-release such that maintenance and quality assurance can cope with the changes in the intended use of an application after release. The testing environment will integrate, adapt and automate various techniques for continuous Future Internet testing (dynamic model inference, model-based testing, log-based diagnosis, oracle learning, combinatorial testing, concurrent testing, regression testing).
Automatisch testen van Java klassen, I.S.W.B. Prasetya, , in the Java Magazine No 2, 2009.
JUnit 4.x Quick Tutorial, I.S.W.B. Prasetya. This tutorial is for novice Java programmers who try to learn JUnit.
Patterns for In-code Algebraic Testing, I.S.W.B Prasetya, T.E.JVos, Technical report UU-CS-2008-037, Dept. of Information and Computing Sciences, Utrecht University, 2008. This paper describes an in-code approach to automatic algebraic-based software testing and a number of useful design patterns for doing it. The approach uses algebras as testable views on a system. These views form test interfaces which are highly automatable. Specifications are expressed in terms of axioms of the algebras. We use the testing tool T2 to provide automation. T2 works with in-code specifications; these are specifications written directly in a programming language. Because in-code specifications do not need any additional skill to master, they are more likely to be adopted by engineers on the field. Because they need no additional tools to parse and to keep them insync with the implementation, they are much cheaper to maintain. So, for real uses they have a good chance to scale up.
Trace-based Reflexive Testing of OO Programs with T2, I.S.W.B Prasetya, T.E.J. Vos, A.I. Baars, in the Proceedings of 1st IEEE International Conference on Software Testing, Verification and Validation (ICST), IEEE, 2008. This paper presents an automatic trace-based unit testing approach to test object-oriented programs. Most automated testing tools test a class C by testing each of its methods in isolation. Such an approach works poorly if specifications are only partial, which is usually the case in practice. In contrast, our approach generates sequences of calls to the methods of C that are checked on-the-fly. This is more interactive, and has the side effect that methods are checking each other. Although simple, it seems to work quite well, even when specifications are only partially provided. We implement the approach in a tool called T2. It targets Java. It can test internal errors, Hoare triple specifications, class invariant, and even temporal properties. Furthermore, T2 accepts 'in-code' specifications, these are specifications written in the specified class itself, and are written in plain Java; hence reducing the cost usually needed to maintain specifications to minimum.

Earlier versions (free):

Trace-based Reflexive Testing of OO Programs, I.S.W.B. Prasetya, J. Amorim, T.E.J. Vos, A. Baars, Tech. Report UU-CS-2007-037, Dept. of Information and Computing Sciences, Utrecht University, 2007.
Incremental Implementation of Syntax Driven Logics, I.S.W.B. Prasetya, A. Azurat, T.E.J. Vos, A.J. van Leeuwen, in Journal of Software, 1(3), 1-13, Academy Publisher, 2006. This paper describes a technique combining higher order functions, algebraic datat ypes, and monads to incrementally implement syntax driven logics. Extensions can be compositionally stacked while the base logic is left unchanged. The technique can furthermore be used to build a set of weaker logics for light weight verification or to generate validation traces. The paper explains the technique through an example: a Hoare logic for a simple command language. The example also shows how exceptions can be treated as an extension, without having to change the underlying logic. This is an extended version of the SEFM version below, and free.
Web Cube, I.S.W.B. Prasetya, T.E.J. Vos, S.D. Swierstra, in the Proceedings of Formal Techniques for Networked and Distributed Systems (FORTE) 2006, LNCS 4229, Springer, 2006. This paper introduces a refinement of Misra’s Seuss logic, called Web Cube, that provides a model for programming and reasoning over web applications. It features black box composition of web services so that services offered by large systems, such as that of a back-end database, can be treated abstractly and consistently. It inherits the light weight feature of Seuss, which relies on an abstract view towards concurrency control, which leads to a less error-prone style of distributed programming, backed by a clean logic.
Building Verification Condition Generators by Compositional Extensions, I.S.W.B. Prasetya, A. Azurat, T.E.J. Vos, A.J. van Leeuwen, in the Proceedings of 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM), 2005.
Formal Design of Self-stabilizing Programs, I.S.W.B Prasetya, S.D. Swierstra, in Journal of Highspeed Network, special issue on self-stabilizing systems, 14(1), IOS Press, 2005. Distributed algorithms, self-stabilizing systems in particular, are often too delicate to be argued informally. Formal proofs are much more reliable, but unfortunately are often long and complicated. Some of the complication is inherent, but some is also the result of poor notation and formalism which is not abstract enough. Improving them would make formal proofs easier to write and to understand, which will also make them less error prone. In this spirit, this paper proposes an extension of the logic UNITY with a number of new operators to model self-stabilization and a formalization of a number of useful design strategies. They should enhance the formalism offered by UNITY with better abstraction to specify and reason about self-stabilization.
Theorem Prover Supported Logics for Small Imperative Languages, I.S.W.B Prasetya, A. Azurat, T.E.J. Vos, A.J. van Leeuwen, H. Suhartanto, Technical report UU-CS-2005-046, Dept. of Information and Computing Sciences, Utrecht University, 2005. This report describes a simple imperative programming language L0 and its logic, which are integrated to the theorem prover HOL through syntactical embedding. The approach allows HOL's own type checker to be reused and its concrete syntax to be, to some degree, customized. The logic of L0 is Hoare-based and is completely syntax driven. Depending on how we limit its assertion language it can be made first order. A possible application of L0 is to use it as a core in rapid prototyping of small imperative languages with integrated verification support. This report gives two examples of new languages built on L0: a language to write a suite of L0-unit tests and a language for scripting database transactions.
LinguSQL: a Verification and Transformation Tool for Database Application, R.W. Purbojati, I.S.W.B Prasetya, S. Maizir, B. Wibowo, and A. Azurat, in Seminar Nasional Ilmu Komputer dan Teknologi Informasi (SNIKTI), 2005. Lingu is an experimental abstract language for programming database scripting. This language includes verification and validation as an integral part of its programming. The verification and validation ensures the application is capable to be used in critical operation. The programming of Lingu itself does not produces a working code, instead it produce an abstract code that describes program logic. This abstract language is transformed into a concrete language, such as C or Java, intended to be used in real operation. This paper discuss about the development of LinguSQL. LinguSQL is a tool for verifying and transforming Lingu script. Currently the development of LinguSQL is in prototyping phase. We hope that the prototype will provide a clear guidance in further development.
Technology for Specifying and Generating Critical Data Processsing Programs, H. Suhartanto, I.S.W.B Prasetya, B. Widjaja, L. Y. Stefanus, A. Azurat, S. Aminah, and J. Bong, in the Proceedings of 8th International Conference on Quality of Research, 2005. Todo: archive is lost!
Towards Reliable Component Software: Light-weight Formalism, A. Azurat and I.S.W.B. Prasetya, in the Proceedings of 8th International Conference on Quality of Research, 2005.
Towards Automated Verification of Database Scripts, A. Azurat, I.S.W.B. Prasetya, T.E.J. Vos, H. Suhartanto, B. Widjaja, L.Y. Stefanus, R. Wenang, S. Aminah, and J. Bong, in the Proceedings of 18th International Conference on Theorem Proving in Higher Order Logics (TPHOL), track Emerging Trends, 2005. Abstract. The article reports on our preliminary research activities towards the verification of database transaction scripts. It gives a first order specification language for database transaction scripts and its accompanying logic. The logic is expressed in terms of weakest pre-condition rules and is quite simple and intuitive. The logic is sound, and, if the underlying basic expression language is limited, specifications in our language are decidable. Tables in a database are usually guarded by various integrity constraints. At the moment the logic only supports single attribute primary key constraint. The language has been embedded in the HOL theorem prover. A verification case study on Student Entrance Test Application is described.
A UNITY-based Framework towards Component Based Systems, I.S.W.B Prasetya, T.E.J. Vos, A. Azurat, S.D. Swierstra, in the Proceedings of 8th International Conference on Principles of Distributed Systems (OPODIS), LNCS 3544, Springer, 2004. Compositionality provides the foundation of software modularity, re-usability and separate verification of software components. One of the known difficulties, when separately verifying components, is producing compositional proofs for progress properties of distributed systems. This paper offers a UNITY-based framework to model distributed applications which are built with a component based approach. The framework enables components to be abstractly specified in terms of contracts. Temporal properties are expressed and proven in the UNITY style. Compositional reasoning about components’ properties, including progress, is supported. The semantical model is simple and intuitive.

Earlier versions (free):

A UNITY-based Framework towards Component Based Systems, I.S.W.B Prasetya, T.E.J. Vos, A. Azurat, S.D. Swierstra, Tech. Report UU-CS-2003-043, Dept. of Information and Computing Sciences, Utrecht University, 2003.
∀UNITY: A HOL Theory of General UNITY, I.S.W.B Prasetya, T.E.J Vos, A. Azurat, S.D. Swierstra, in the Proceedings of 16th International Conference on Theorem Proving in Higher Order Logics (TPHOL), track Emerging Trends, p159 - 174, 2003. UNITY is a simple programming logic that can be used to reason about distributed systems. It is especially attractive because of its elegant axiomatical style. Its expresiveness is however limited, and for specific applications people often need variants of UNITY that offer extended or modified logic [23,6,27,16,21,10,20]. When modifying a logic mistakes eas ily creep in: a seemingly very logical new inference rule may turn out to be unsound. Formal verification is often necessary, but it is a time consuming task. ∀UNITY is a generalization that provides the same set of inference rules UNITY does. However, these inference rules are now derived from ∀UNITY’s primitive rules that are weaker than the original ones. Consequently, a UNITY variant (or instance) can be created quickly just by proving that the instance upholds ∀UNITY primitive rules. The resulting UNITY variant is guaranteed to be sound since ∀UNITY is provided as a library within the HOL theorem prover, and all its derived rules are mechanically verified. Moreover, general application theories, such as theories about self-stabilization, can now be written based on ∀UNITY; the theories will automatically extend to all ∀UNITY instances.
A Theory for Composing Distributed Components Based on Temporary Interface, I.S.W.B Prasetya, T.E.J Vos, S.D. Swierstra, B. Widjaja, in the Proceedings of the Workshop on Formal Aspects of Component Software (FACS). 2003. Compositionality provides the foundation of software modularity, re-usability and separate verification of software components. One of the known difficulties, when separately verifying components, is producing compositional proofs for progress properties of distributed systems. This paper presents a composition theory which is based on reasoning about temporary interference. It is not a general theory; it restricts components to take turn when updating common resources, though in exchange it is more powerful. It produces constraints that are informative for implementators, and relatively light weight for verification. It is axiomatic, capturing aspects relevant for composition in a direct and clean way; resulting in a theory which is easy to understand. The theory has been mechanically verified with respect to a UNITY semantics. Extension is in principle possible
Factorizing Fault Tolerance, I.S.W.B Prasetya, S.D. Swierstra, in Journal of Theoretical Computer Science, Special Edition on Dependable Computing 290 (2) p. 1201-1222, 2002. This paper presents a theory of component based development for exception-handling in fault tolerant systems. The theory is based on a general theory of composition, which enables us to factorize the temporal specification of a system into the specifications of its components. This is a new development because in the past efforts to set up such a theory have always been hindered by the problem of composing progress properties.
A Preliminary Report on xMECH, A. Azurat, I.S.W.B. Prasetya, Technical report No. UU-CS-2002-008, Dept. of Information and Computing Sciences, Utrecht University, 2002. This document reports the current development status of xMECH. It is an implementation of the so-called skin or hybrid embedding approach for HOL. Its purpose is to enhance HOL's power and interaction to do software veri¯cation. xMECH features languages and logics to describe and verify sequential and distributed programs, a reasonably rich expression language to write specifications, and optimized verification condition generators. It is available for public use, but it is still in a prototype phase, with limited features and user support. It comes with some simple demos, but doing a serious project with xMECH is not (yet) recommended for an inexperienced user
Survey on Embedding Programming Logics in a Theorem Prover, A. Azurat, I.S.W.B. Prasetya, Technical report No. UU-CS-2002-007, Dept. of Information and Computing Sciences, Utrecht University, 2002. Theorem provers were also called ’proof checkers’ because that is what they were in the beginning. They have grown powerful, however, capable in many cases to automatically produce complicated proofs. In particular, higher order logic based theorem provers such as HOL and PVS became popular because the logic is well known and very expressive. They are generally considered to be potential platforms to embed a programming logic for the purpose of formal verification. In this paper we investigate a number of most commonly used methods of embedding programming logics in such theorem provers and expose problems we discover. We will also propose an alternative approach : hybrid embedding.
Embedding Programming Logics in HOL Theorem Prover, I.S.W.B. Prasetya, A. Azurat, S.D. Swierstra, in Jurnal Ilmu Komputer dan Teknologi Informasi 2 (1), 2002. Todo: the Journal archive is lost!
Sebuah Framework untuk Mekanisasi Multi Logika, I.S.W.B. Prasetya, A. Azurat, S.D. Swierstra, B. Widjaja, in Jurnal Ilmu Komputer dan Teknologi Informasi 1 (2), 2001. Todo: the Journal archive is lost!
Mechanically Verified Self-Stabilizing Hierarchical Algorithms, I.S.W.B. Prasetya, in the Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS) Conference, LNCS 1217, 1997. This paper investigates self-stabilization on hierarchically divided networks. An underlying theory of self-stabilizing systems will be briefly exposed and a generic example will be given. The example and the theory have been mechanically verified using a general purpose theorem prover HOL. Three issues inherent to the problem, namely self-stabilization, concurrency, and hierarchy, can be factored out and treated one separately — something which has considerably simplified our mechanical proof (proof economy is an important issue in mechanical verification, even more than it is in the pencil and paper realm as what misleadingly appears as a few lines there may easily become a few hundreds in the mechanical world).
Formal methods and mechanical verification applied to the development of a convergent distributed sorting program, T.E.J. Vos, S. D. Swierstra, S. W. B. Prasetya, Tech. Report UU-CS-1996-37, Dept. of Information and Computing Sciences, Utrecht University, 1996.
Error in the UNITY Substitution Rule for Subscripted Operators, I.S.W.B. Prasetya, in Formal Aspects of Computing 6, pp. 466-470, 1994. UNITY, introduced by Chandy and Misra [ChM88], is a programming logic intended to reason about temporal properties of distributed programs. Despite the fact that UNITY does not have the full power of, for example, linear temporal logic, it enjoys popularity due to its simplicity. There was however a serious problem with the Substitution Rule. The logic is incomplete without the rule, and with the rule it is inconsistent. Latterly Beverly Sanders introduced the concept of strongest invariant and proposed a new definition for UNITY [San91] that fixes the problem with the Substitution Rule. For the benefit of program union, she also introduced the concept of subscripted properties and claimed a generalized version of Substitution Rule for the subscripted properties. This report presents an example that shows that the latter claim is false. A proposal as how to fix this follows.
Towards a Mechanically Supported and Compositional Calculus to Design Distributed Algorithms, I.S.W.B. Prasetya, in the Proceedings of International Conference on Theorem Proving in Higher Order Logics (TPHOL), LNCS 859, 362-377, 1994. This paper presents a compositional extension of the programming calculus UNITY, which is used to design distributed programs. As the extension is compositional, we can use it to derive a program ’on the fly’. That is, we can shape a program at the same time as we manipulate and decompose its given specification, and each time we apply a compositionality theorem we basically add a detail to the shape. Safety properties are known to be compositional in UNITY, but progress in general are not. So, we define a class of progress properties which are compositional. In addition, for programs that are constructed from components that do not write each other's write variables, the compositionality of this new class of progress can be expressed elegantly. We also have formalized and verified the resulting calculus using the theorem prover HOL. Together with the available tools in HOL this provides a mechanical support in designing distributed programs.
A Formal Approach to Design Self-stabilizing Programs, I.S.W.B. Prasetya, in the Proceedings of Computing Science in the Netherlands (CSN), 1994, pages 241-252. Todo: archive is lost!
On the Style of Mechanical Proving, I.S.W.B. Prasetya, in the Proceedings of International Conference on Theorem Proving in Higher Order Logics (TPHOL), LNCS 780, pp. 475-488, 1993. It is quite surprising that — after 5 years of experience — there has been still very little written about how to present and construct mechanical proofs. Such guidelines would definitely help a novice. Since mechanical proving is very different from proving on paper, it may take a long time before one gets accustomed to it and develops an efficient style for constructing and presenting such proofs. Traditional styles, like e.g. decomposing a problem into lemmas and incorporating hints to make the logic of a proof visible, are not straightforwardly taken over to the HOL world. In this paper we present two extensions to HOL, the DERIVATION and LEMMA packages, by which proofs can be written in very much the same format as one would on paper. They are not intended as a replacement of existing HOL mechanisms, but rather as an extension for enabling work in a higher level proof environment.
Formalization of Variables Access Constraints to Support Compositionality of Liveness Properties, I.S.W.B. Prasetya, in the Proceedings International Conference on Theorem Proving in Higher Order Logics (TPHOL), LNCS 780, pp. 324-337, 1993. Because reasoning about programs' liveness behavior is difficult people become interested in the potential of theorem provers to aid verification. In extending a theorem prover with a lifeness logic it would be nice if compositionality is also supported since it is a property of a great practical interest: it allows modularity in design. However, a straightforward extension that only embodies the essence of the logic will fail to do so. In implementing such an extension we should therefore be aware of the technical details required for compositionality. In particular, compositionality of progress under parallel composition depends on the concept of variable accessibility. Therefore, this concept has to be explicitly present in the extension. This paper is about the formalization of access constraints to support compositionality.
Sistem Penghitungan Suara Pemilu Multi Sekuriti, I.S.W.B. Prasetya, Technical report UI-CS-1977-01, Faculty of Computer Science, University of Indonesia, 1997. Karya tulis ini membahas konsep dan rancangan sistem pencacahan suara multi sekuriti untuk Pemilu Indonesia. Rancangan tersebut didasarkan pada teknologi mutakhir sekuriti digital yang memungkinkan pengesahan data yang tidak bisa dibantah dan tidak bisa dipalsu. Teknologi seperti ini secara drastis mengeliminasi berbagai kelemahan sekuriti sistem konvensional, khususnya kelemahan-kelemahan sekuriti yang memungkinkan dilakukannya kecurangan oleh pihak-pihak tak bertanggung jawab. Aspek yang juga penting dari rancangan kami adalah bahwa hasil penghitungan dapat di uji-silang oleh pihak independen tanpa membahayakan integritas data penghitungan. Dengan cara demikian, pihak penyelenggara Pemilu dapat dengan mudah membuktikan kejujurannya apabila dihadapkan pada tuduhan kecurangan. Perhatian juga diberikan pada aspek ekonomis. Sistem dirancang sesederhana mungkin dan menggunakan komponen-komponen yang diproduksi masal di pasar dunia (bukan produk khusus) sehingga murah harganya. Keyakinan kami adalah bahwa sistem ini bisa direalisasi dengan biaya yang relatif murah

Recent Papers


Projects

FITTEST: FP7 EU project no-257574 on Future Internet Testing, 2011-13.

Read more Software

JUnit 4.x Quick Tutorial

Read more
If software can lie, will it feel guilty?
Original CSS by marija zaric