Formal methods (FM)
Key persons
J. Vain, J. Ernits
Publications 2008
- A. Anier. Motion recognition with abstract interpretation and HMM.
In Proc. of 11th Biennial Baltic Electronics Conf., BEC 2008
(Tallinn, Oct. 2008), pp. 191-194. Tallinn Univ. of Techn.,
2008. doi:
10.1109/bec.2008.4657511 (WOS:
0002609949000381, Scopus: 2-s2.0-57849085845)
- J. Ernits, M. Kääramees, K. Raiend, A. Kull.
Requirements-driven model-based testing of the IP multimedia
subsystem. In Proc. of 11th Biennial Baltic Electronics Conf., BEC
2008 (Tallinn, Oct. 2008), pp. 203-206. Tallinn Univ. of Techn.,
2008. doi:
10.1109/bec.2008.4657514 (WOS:
000260994900041, Scopus: 2-s2.0-57849120370)
- J. Ernits, M. Veanes, J. Helander. Model-based testing of robots
with NMmodel. In K. Suzuki, T. Higashino, A. Ulrich, eds., Short
Papers of TESTCOM/FATES 2008 (Tokyo, June 2008),
pp. 40-49. 2008.
- J. Jakubiak, S. Nõmm, J. Vain, F. Miyawaki. Polynomial based
approach in analysis and detection of surgeon's motions. In
Proc. of 10th Int. Conf. on Control, Automation, Robotics and
Vision, ICARCV 2008 (Hanoi, Dec. 2008), pp. 611-616. IEEE CS
Press, 2008. doi:
10.1109/icarcv.2008.4795588 (WOS:
000266716600107, Scopus: 2-s2.0-64549102455)
- T. Kirt. Fast and adaptive scheduling in ad hoc networks. In
Proc. of 11th Biennial Baltic Electronics Conf., BEC 2008 (Tallinn,
Oct. 2008), pp. 251-254. Tallinn Univ. of Techn., 2008. doi:
10.1109/bec.2008.4657527 (WOS:
000260404800014, Scopus: 2-s2.0-57849148677)
- S. Nõmm, E. Petlenkov, J. Vain, J. Belikov, F. Miyawaki, K.
Yoshimitsu. Recognition of the surgeon's motions during endoscopic
operation by statistics based algorithm and neural networks based
ANARX models. In M. J. Chung, P. Misra, H. Shim, eds., Proc. of
17th IFAC World Congress (Seoul, July 2008). 2008. (Scopus: 2-s2.0-79961020009)
- K. Oiinuma, K. Masamune, T. Sadaiiiro, K. Yosihimitsu, J. Vain,
D. Hashimoto, Y. Fukui, F. Miyawaki. Intraoperative analysis of
surgeon's motions and construction of timed automata based model of
laparoscopic surgery for human-adaptive surgical robot
system. Trans. of Soc. of Instrum. and Control Eng., v. 43,
n. 8, pp. 679-688, 2008.
- E. Petlenkov, S. Nõmm, J. Vain, F. Miyawaki. Application of
self-organizing Kohonen map to detection of surgeon motions during
endoscopic surgery. In Proc. of 2008 Int. Joint Conf. on Neural
Networks, IJCNN 2008 (2008 IEEE World Congress on Computational
Intelligence, WCCI 2008, Hong Kong, June 2008),
pp. 2806-2811. IEEE CS Press, 2008. doi:
10.1109/ijcnn.2008.4634193 (WOS:
000263827201189, Scopus: 2-s2.0-56349119450)
- T. Tammet, J. Vain, A. Puusepp, E. Reilent, A. Kuusik. RFID-based
communications for a self-organizing robot swarm. In S. Brueckner,
P. Robertson, U. Bellur, eds., Proc. of 2nd IEEE Int. Conf. on
Self-Adaptive and Self-Organizing Systems, SASO 2008 (Venice,
Oct. 2008), pp. 45-54. IEEE CS Press, 2008. doi:
10.1109/saso.2008.62 (WOS:
000262480300006, Scopus: 2-s2.0-57949087105)
- J. Vain, F. Miyawaki. Model learning for reactive motion planning
in assisting robots. In L. Bruzzone, ed., Proc. of 27th IASTED
Int. Conf. on Modelling, Identification and Control, MIC 2008
(Innsbruck, Feb. 2008), 6 pp. Acta Press, 2008.
- J. Vain, T. Tammet, A. Kuusik, S. Juurik. Towards scalable proofs
of robot swarm dependability. In Proc. of 11th Biennial Baltic
Electronics Conf., BEC 2008 (Tallinn, Oct. 2008),
pp. 199-202. Tallinn Univ. of Techn., 2008. doi:
10.1109/bec.2008.4657513 (WOS:
000260994900040, Scopus: 2-s2.0-57849099321)
- J. Vain, T. Tammet, A. Kuusik, E. Reilent. Software architecture
for swarm mobile robots. In Proc. of 11th Biennial Baltic
Electronics Conf., BEC 2008 (Tallinn, Oct. 2008),
pp. 231-234. Tallinn Univ. of Techn., 2008. doi:
10.1109/bec.2008.4657522 (WOS:
000260994900049, Scopus: 2-s2.0-57849117120)
Publications 2009
- J. P. Ernits, R. Dearden, M. Pebody. Formal methods for automated
diagnosis of Autosub 6000. In E. Denney, D. Giannakopoulou,
C. S. Pasareanu, eds., Proc. of 1st NASA Symp. on Formal Methods,
NFM 2009 (Moffett Field, CA, Apr. 2009), pp. 181-185. NASA Ames
Research Center, 2009. proceedings
volume at conference website
- J. Ernits, R. Roo, J. Jacky, M. Veanes. Model-based testing of
web applications using NModel. In M. Nunez, P. Baker, M. G. Merayo,
eds., Proc. of 21st IFIP WG 6.1 Int. Conf. on Testing of
Communicating Systems and 9th Int. Wksh. on Formal Approaches to
Testing of Software, TESTCOM/FATES 2009 (Eindhoven, Nov. 2009),
v. 5826 of Lect. Notes in Comput. Sci., pp. 211-216. Springer,
2009. doi:
10.1007/978-3-642-05031-2_14 (WOS:
000276634800014, Scopus: 2-s2.0-70549109216)
- M. Kääramees, R. Paaslepp. Using text categorisation for detecting
user activity. In A. P. Abraham, ed., Proc. of IADIS Europ. Conf,
on Data Mining 2009, ECDM '09 (Algarve, June 2009),
pp. 139-142. IADIS Press, 2009. (Scopus:
2-s2.0-77955625860)
- A. Kull, K. Raiend, J. Vain, M. Kääramees. Case study-based
performance evaluation of reactive planning tester. In T. Bauer,
H. Eichler, A. Rennoch, S. Wieczorek, eds., Proc. of 2nd Wksh. on
Model-Based Testing in Practice, MoTiP 2009 (Enschede, June 2009),
v. WP09-08 of CTIT Wksh. Proc. Series, pp. 87-96. 2009. proceedings
volume at Fraunhofer Fokus website
- S. Nõmm, J. Vain, E. Petlenkov, F. Miyawaki, K. Yoshimitsu. Hybrid
approach to detection of the surgeon's hand motions during endoscope
surgery. In Proc. of 4th IEEE Conf. on Industrial Electronics and
Applications, ICIEA '09 (Xi'an, May 2009), pp. 3488-3492. IEEE,
2009. doi:
10.1109/iciea.2009.5138854 (WOS:
000273183201298, Scopus: 2-s2.0-70349308712)
- J. Vain, F. Miyawaki, S. Nõmm, T. Totskaya,
A. Anier. Human-robot interaction learning using timed automata. In
Proc. of ICROS-SICE Int. Joint Conf. ICCAS-SICE 2009 (Fukuoka,
Aug. 2009), pp. 2037-2043. Soc. of Instrum. and Contr. Eng.,
2009. article
at IEEE Xplore (Scopus:
2-s2.0-77951126757)
- J. Vain, S. Nõmm, A. Anier, F. Miyawaki, T. Totskaya. Supervised
training of voting automata for the surgeon's motion recognition
during laparoscope surgery. In Proc. of 2009 IEEE Int. Conf. on
Control and Automation, ICCA '09 (Christchurch, Dec. 2009),
pp. 1503-1508. IEEE, 2009. doi:
10.1109/icca.2009.5410373 (WOS:
000280542300261, Scopus: 2-s2.0-77950421829)
Publications 2010
- A. Anier, J. Vain. Timed automata based provably correct
robot control. In Proc. of 12th Biennial Baltic Electronics Conf.,
BEC 2010 (Tallinn, Oct. 2010), pp. 201-204. IEEE, 2010. doi:
10.1109/bec.2010.5631008 (Scopus:
2-s2.0-79952142799)
- J. P. Ernits, R. Dearden, M. Pebody. Automatic fault
detection and execution monitoring for AUV missions. In Proc. of
2010 IEEE Conf. on Autonomous Underwater Vehicles, AUV 2010 (Monterey,
CA, Sept. 2010), 9 pp. IEEE, 2010. doi:
10.1109/auv.2010.5779660 (Scopus:
2-s2.0-79960689313)
- J. P. Ernits, R. Dearden, M. Pebody,
J. Guggenheim. Diagnosis of Autosub 6000 using automatically generated
component models. In
Proc. of 21st Int. Wksh. on Principles of Diagnosis, DX 2010
(Portland, OR, Oct. 2010), 8 pp. Prognostics and Health Management
Society, 2010. article
at publisher's website
- M. Kääramees, J. Vain, K. Raiend. Model-based synthesis of
reactive planning on-line testers for non-deterministic embedded
systems. In Proc. of 12th Biennial Baltic Electronics Conf., BEC
2010 (Tallinn, Oct. 2010), pp. 189-192. IEEE, 2010. doi:
10.1109/bec.2010.5631735 (Scopus:
2-s2.0-79952160362)
- M. Kääramees, J. Vain, K. Raiend. Synthesis of on-line planning
tester for non-deterministic EFSM models. In L. Bottaci, G. Fraser,
eds., Proc. of 5th Testing: Academic and Industrial Conf.: Practice
and Research Techniques, TAIC PART 2010 (Windsor, Sept. 2010),
v. 6303 of Lect. Notes in Comput. Sci., pp. 147-154. Springer,
2010. doi:
10.1007/978-3-642-15585-7_14 (WOS:
000286284100014, Scopus: 2-s2.0-78149267145)
- M. Matskin, J. Haeverin, J. Roning, J. Vain. Cloud computing with
robots: does it make sense? In A. J. Berre, A. Sadovykh,
F. M. Federico, D. Roman, eds., Proc. of Wksh. on Modeling, Design,
and Analysis for the Service Cloud Workshop, Mda4ServiceCloud '10
(Paris, June 2010), 2 pp. A CEA LIST publication, 2010.
- S. Nõmm, A. Leibak, J. Vain, F. Miyawaki. Application of volume
bounding box decomposition for surgeon's hand gestures recognition. In
Proc. of 36th Ann. Conf. of IEEE Industrial Electronics Society,
IECON 2010 (Phoenix, AZ, Nov. 2010), pp. 1076-1080. IEEE,
2010. doi:
10.1109/iecon.2010.5675518 (WOS:
000300146000013, Scopus: 2-s2.0-78751469437)
- S. Nõmm, J. Vain, F. Miyawaki. Towards application of
coordinate invariant approach in detection of the surgeon hand
gestures during laparoscope surgery. In Proc. of 2010 Int. Congress
on Computer Applications and Computational Science, CACS 2010
(Singapore, Dec. 2010), pp. 1036-1038. IRAST, 2010.
- K. Parm, S. Nõmm, J. Vain. Application of bidding automata
for measuring the informativeness of hand motion characteristic
features. In Proc. of 12th Biennial Baltic Electronics Conf.,
BEC 2010 (Tallinn, Oct. 2010), pp. 205-208. IEEE, 2010. doi:
10.1109/bec.2010.5631639 (Scopus:
2-s2.0-79952178487)
Publications 2011
- J. P. Ernits, R. Dearden. Towards diagnosis modulo
theories. In M. Sachenbacher, O. Dressler, M. Hofbaur, eds.,
Proc. of 22nd Int. Wksh. on Principles of Diagnosis, DX 2011
(Murnau, Oct. 2011), pp. 249-256. TU München, 2011. volume
at publisher's website
- J. P. Ernits, R. Dearden, M. Pebody. Fault diagnosis
challenge in a flight-class autonomous underwater vehicle. In
M. Sachenbacher, O. Dressler, M. Hofbaur, eds.,
Proc. of 22nd Int. Wksh. on Principles of Diagnosis, DX 2011
(Murnau, Oct. 2011), pp. 175-178. TU München, 2011. volume
at publisher's website
- J. P. Ernits, C. Gretton, R. Dearden. AYALSOPLAN: bitstate
pruning for state-based planning on massively parallel computer
clusters. In Á. García-Olaya, S. Jiménez, C. Linares López, eds.,
Description of Participating Planners of 7th Int. Planning
Competition (Madrid, July 2011), pp. 117-124. Universidad Carlos
III de Madrid, 2011. handle: 10016/11710
- S. Juurik, J. Vain. Model checking emerging behavior
properties of robot swarms. Proc. of Estonian Acad. Sci.,
v. 60, n. 1, pp. 48-54, 2011. doi:
10.3176/proc.2011.1.05 (WOS:
000287601700005, Scopus: 2-s2.0-79951864143)
- J. Vain, A. Kull, M. Kääramees, M. Markvardt, K. Raiend.
Synthesis of test purpose directed reactive planning tester for
nondeterministic systems. In J. Zander, I. Schieferdecker,
P. J. Mosterman, eds., Model-Based Testing for Embedded
Systems, Computational Analysis, Synthesis, and Design of
Dynamic Systems, pp. 425-452. CRC Press, 2011.
Publications 2012
- D. Ahman, M. Kääramees. Constraint-based heuristic on-line
test generation from non-deterministic I/O EFSMs. In A. K. Petrenko,
H. Schlingloff, eds., Proc. of 7th Wksh. on Model-Based
Testing, MBT 2012 (Tallinn, March 2012), v. 80 of
Electron. Proc. in Theor. Comput. Sci., pp. 115-129. Open
Publishing Assoc., 2012. doi:
10.4204/eptcs.80.9 (Scopus:
2-s2.0-84959354689)
- A. Anier, J. Vain. Model based continual planning and
control for assistive robots. In E. Conchon et al., eds.,
Proc. of Int. Conf. on Health Informatics, HEALTHINF 2012
(Vilamoura, Feb. 2012), pp. 382-385. SciTePress, 2012. doi:
10.5220/0003783503820385 (Scopus:
2-s2.0-84861994976)
- A. Anier, J. Vain. Model based continual planning and
control framework for assistive robots. In C. Benavente-Peces et al.,
eds., Proc. of 2nd Int. Conf. on Pervasive and Embedded Computing
and Communication Systems, PECCS 2012 (Rome, Feb. 2012),
pp. 403-406. SciTePress, 2012. doi:
10.5220/0003827104030406 (Scopus:
2-s2.0-84862141624)
- J. Berthing, P. Boström, K. Sere, L. Tsiopoulos,
J. Vain. Refinement-based development of timed systems. In
J. Derrick, S. Gnesi, D. Latella, H. Treharne, eds., Proc. of 9th
Int. Conf. on Integrated Formal Methods, IFM 2012 (Pisa, June
2012), v. 7321 of Lect. Notes in Comput. Sci.,
pp. 69-83. Springer, 2012. doi:
10.1007/978-3-642-30729-4_6 (Scopus:
2-s2.0-84864333404)
- K. Sarna, J. Vain. Exploiting aspects in model-based
testing. In Proc. of 11th Wksh. on Foundations of Aspect-Oriented
Languages, FOAL '12 (Potsdam, March 2012), pp. 45-47. ACM
Press, 2012. doi:
10.1145/2162010.2162023 (Scopus:
2-s2.0-84860482936)
- J. Vain, E. Halling. Constraint-based test scenario
description language. In Proc. of 13th Biennial Baltic Electronics
Conf., BEC '12 (Tallinn, Oct. 2012), pp. 89-92. Tallinn
Univ. of Techn., 2012. doi: 10.1109/bec.2012.6376822 (Scopus: 2-s2.0-84873286590)
- J. Vain, M. Kääramees, M. Markvardt. Online testing of
nondeterministic systems with reactive planning tester. In L. Petre,
K. Sere, E. Troubitsyna, eds., Dependability and Computer
Engineering: Concepts for Software-Intensive Systems,
pp. 113-150. IGI Global, 2012. doi:
10.4018/978-1-60960-747-0.ch007 (WOS:
000363423800008, Scopus: 2-s2.0-84860447190)
Publications 2013
- R. Dearden, J. Ernits. Automated fault diagnosis for an
autonomous underwater vehicle. IEEE J. of Oceanic Engin.,
v. 38, n. 3, pp. 484-499, 2013. doi:
10.1109/joe.2012.2227540 (WOS:
000321925500008, Scopus: 2-s2.0-84880569717)
- H. Liu, H, J. Vain. An agent-based modeling for
price-responsive demand simulation. In S. Hammoudi et al., eds.,
Proc. of 15th Int. Conf. on Enterprise Information Systems,
ICEIS 2013 (Angers, July 2013), v. 1,
pp. 405-412. SciTePress, 2013. doi:
10.5220/0004417504360443 (WOS:
000349992200053, Scopus: 2-s2.0-84887787431)
- S. Srinivasan, R. Kumar, J. Vain. Integration of IEC 61850
and OPC UA for smart grid automation. In Proc. of Innovative Smart
Grid Technologies Conf. Asia, ISGT-ASIA 2013 (Bangalore,
Nov. 2013), 5 pp. IEEE, 2013. doi:
10.1109/isgt-asia.2013.6698789 (WOS:
000330237600090, Scopus: 2-s2.0-84893232790)
Publications 2014
- E. Brezhniev, V. Kharchenko, J. Vain. Cyber security of smart
substations with critical load via cyber diversity: strategies and
assessment. In Proc. of 12th IEEE East-West Design and Test
Symposium, EWDTS '14 (Kiev, Sept. 2014), pp. 26-29. IEEE,
2014.
- V. Kharchenko, O. Illiashenko, A. Boyarchuk, C. Phillips,
J. Vain, M. Krispin. FPGA-based critical computing: TEMPUS and
FP7 projects issues. In Proc. of 10th European Wksh. on
Microelectronics Education, EWME '14 (Tallinn, May 2014),
pp. 74-79. Tallinn Univ. of Techn./IEEE, 2014. doi:
10.1109/ewme.2014.6877399 (WOS:
000345757100016, Scopus: 2-s2.0-84906724480)
- P. Lump, J. Ernits, J. Vain. Towards better
specifications for software outsourcing. In H.-M. Haav, A. Kalja,
T. Robal, eds.,
Proc. of 11th Int. Baltic Conf. on Databases and Information
Systems, Baltic DB&IS 2014 (Tallinn, June 2014),
pp. 453-458. Tallinn Univ. of Techn., 2014.
- K. Sarna, J. Vain. Aspect-oriented testing of a
rehabilitation system. In Proc. of 6th Int. Conf. on Advances in
System Testing and Validation Lifecycle, VALID 2014 (Nice,
Oct. 2014), pp. 73-78. XPS, 2014. article
in ThinkMind DL (Scopus:
2-s2.0-84922728350)
- S. Srinivasan, F. Buonopane, S. Ramaswamy,
J. Vain. Verifying response times in networked automation
systems using jitter bounds. In
Proc. of 25th IEEE Int. Symp. on Software Reliability Workshops,
ISSREW '14 (Naples, Nov. 2014), pp. 47-50. IEEE, 2014. doi:
10.1109/issrew.2014.42 (WOS:
000360286200012, Scopus: 2-s2.0-84922627954)
- D. Truscan, J. Vain, M. Koskinen. Combining
aspect-orientation and UPPAAL timed automata. In A. Holzinger et al.,
eds., Proc. of 9th Int. Conf. on Software Paradigm Trends,
ICSOFT-PT 2014 (Vienna, Aug. 2014), pp. 159-164. SciTePress,
2014. doi:
10.5220/0005105101590164 (Scopus:
2-s2.0-84908873809)
- J. Vain, A. Anier, E. Halling. Provably correct test
generation for online testing of timed systems. In H.-M. Haav,
A. Kalja, T. Robal, eds., Proc. of 11th Int. Baltic Conf. on
Databases and Information Systems, Baltic DB&IS 2014
(Tallinn, June 2014), pp. 337-348. Tallinn Univ. of Techn.,
2014.
- J. Vain, A. Anier, E. Halling. Provably correct test
generation for online testing of timed systems. In H.-M. Haav,
A. Kalja, T. Robal, eds. Databases and Information Systems
VIII, v. 270 of Frontiers in Artificial Intelligence,
pp. 289-302. IOS Press, 2014. doi:
10.3233/978-1-61499-458-9-289 (WOS:
000362357700021, Scopus: 2-s2.0-84911488779)
- J. Vain, H. Sarapuu. Towards context-sensitive dialogue
with robot companion. In Proc. of 14th Biennial Baltic Electronics
Conference, BEC '14 (Tallinn, Oct. 2014), pp. 205-208. Tallinn
Univ. of Techn./IEEE, 2014. doi:
10.1109/bec.2014.7320592 (Scopus:
2-s2.0-84971249923)
Publications 2015
- J. Ernits, E. Halling, G. Kanter, J. Vain.
Model-based integration testing of ROS packages: a mobile robot case
study. In Proc. of 2015 IEEE Europ. Conf. on Mobile Robots,
ECMR 2015 (Lincoln, Sept. 2015), 7 pp. IEEE, 2015. doi:
10.1109/ecmr.2015.7324210 (Scopus:
2-s2.0-84962218679)
- S. Srinivasan, F. Buonopane, J. Vain, S. Ramaswamy. Model
checking response times in networked automation systems using jitter
bounds. Computers in Industry, v. 74, pp. 186-200, 2015. doi:
10.1016/j.compind.2015.06.012 (WOS:
000364893000015, Scopus: 2-s2.0-84941729353)
- D. Truscan, J. Vain, M. Koskinen, J. Iqbal. A
tool-supported approach for introducing aspects in UPPAAL timed
automata. In A. Holzinger, J. Cardoso, J. Cordeiro, T. Libourel,
L. A. Maciaszek, M. van Sinderen, eds., Revised Selected Papers
from 9th Int. Joint Conf. on Software Technologies,
ICSOFT 2014 (Vienna, Aug. 2014), v. 555 of
Commun. in Comput. and Inform. Sci., pp. 349-364. Springer,
2015. doi:
10.1007/978-3-319-25579-8_20 (WOS:
000369296800020, Scopus: 2-s2.0-84951200780)
- J. Vain, L. Tsiopoulos, P. Bostöm. Integrating
refinement-based methods for developing timed systems. In L. Petre,
E. Sekerinski, eds., From Action Systems to Distributed Systems:
The Refinement Approach, CRC Press, to appear.
Last update 24 June 2016