Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
malta13 [2013/06/17 15:55] pace |
malta13 [2013/06/19 23:32] cesar.sanchez |
||
|---|---|---|---|
| Line 11: | Line 11: | ||
| === Sunday, 16 June 2013 === | === Sunday, 16 June 2013 === | ||
| + | |||
| + | |||
| | 10.00-10.30 | //Christian Colombo:// Verifying Web Applications: From Business Level Specifications to Automated Model-Based Testing | | | 10.00-10.30 | //Christian Colombo:// Verifying Web Applications: From Business Level Specifications to Automated Model-Based Testing | | ||
| - | | 10.30-11.00 | //Julian Samborski-Forlese:// TBA | | + | | 10.30-11.00 | //Julian Samborski-Forlese:// Simulation Relations for Rich Acceptance Conditions | |
| | 11.00-11.30 | **Coffee break** | | | 11.00-11.30 | **Coffee break** | | ||
| | 11.30-12.00 | //Tarmo Uustalu:// Coinductive big-step semantics for concurrency | | | 11.30-12.00 | //Tarmo Uustalu:// Coinductive big-step semantics for concurrency | | ||
| Line 30: | Line 32: | ||
| | 09.00-10.00 | Invited Speaker: **Manuel Hermenegildo** | | | 09.00-10.00 | Invited Speaker: **Manuel Hermenegildo** | | ||
| | 10.00-10.30 | **Coffee break** | | | 10.00-10.30 | **Coffee break** | | ||
| - | | 10.30-11.00 | //Tewodros Beyene:// Solving Existentially Quantfied Horn Clauses | | + | | 10.30-11.00 | {{:malta13-beyene.pdf|//Tewodros Beyene:// Solving Existentially Quantfied Horn Clauses}} | |
| | 11.00-11.30 | //Boriss Selajev:// Scaling dynamic logic for intermediate states | | | 11.00-11.30 | //Boriss Selajev:// Scaling dynamic logic for intermediate states | | ||
| | 11.30-12.00 | //Ondrej Lengal:// Fully Automated Shape Analysis Based on Forest Automata | | | 11.30-12.00 | //Ondrej Lengal:// Fully Automated Shape Analysis Based on Forest Automata | | ||
| Line 104: | Line 106: | ||
| //Christian Colombo// | //Christian Colombo// | ||
| + | While the verification of web-based applications is crucial due to their often security-critical nature, it is considerably challenging due to their complex and dynamical nature. The current state of the art involves automated test execution where a test platform automatically interacts with a web application and asserts the expected behaviour. Still, test cases are typically generated manually, particularly when it comes to directing the test to exercise particular execution paths. In this presentation, we propose a novel combination of the QuickCheck testcase generation tool with web-based applications: QuickCheck exploits an executable automata-based specification to drive and assert the application in an automated yet non-random fashion. However, writing the specification is non-trivial and requires manual intervention. To this end, we propose a means of generating QuickCheck specifications from Cucumber specifications – a commonly used high level specification language for communicating with business stakeholders. | ||
| ---- | ---- | ||